Confluence in number-theoretic rewriting systems
Frédéric Blanqui
frederic.blanqui at inria.fr
Tue Oct 12 02:14:28 EDT 2021
Hello. I invite you to have a look at more recent results on confluence.
For instance, the results of Vincent van Oostrom
(http://cl-informatik.uibk.ac.at/members/vincent/). See
https://dblp.uni-trier.de/pid/69/3031.html and more specifically
https://doi.org/10.1007/978-3-540-70590-1_21, one of his papers on
confluence by decreasing diagrams: "The decreasing diagrams technique is
a complete method to reduce confluence of a rewrite relation to local
confluence. Whereas previous presentations have focussed on the /proof/
the technique is correct, here we focus on /applicability/. We present a
simple but powerful generalisation of the technique, requiring peaks to
be closed only by conversions instead of valleys, which is demonstrated
to further ease applicability." You may also be interested in submitting
your problem on the rewriting at ens-lyon.fr mailing list, and the
confluence competition (http://project-coco.uibk.ac.at/). Best regards,
Frédéric.
Le 05/10/2021 à 02:50, José Manuel Rodríguez Caballero a écrit :
> Dear FOM members,
> The study of whether a string rewriting system is confluent is a
> problem relevant to the fundamentals of mathematics and computer
> science. There are many famous results in this direction, eg the
> Church-Rosser theorem [1] for lambda calculus, Matsumoto theorem [2]
> for Coxeter groups. I would like to ask if there is a known method of
> deciding confluence in the following class of rewriting systems.
>
> Consider the substitution rules:
>
> Rule 0: replace x by a*x + b
>
> Rule 1: replace x by c*x + d
>
> where (a, b, c, d) are positive integers. For simplicity, I will write
> x --> {a x + b, c x + d}. Assume that the domain of x is the set of
> positive integers. The properties of this rewriting system are tightly
> dependent on the arithmetical properties of the parameters. For
> example, it is easy to prove that
>
> x --> { 4 x + 3, 2 x + 1 }
>
> is confluent and its graph is grid-like (code in Mathematica to obtain
> this graph):
>
> NestGraph[{4*#+3, 2*#+1} &, 1, 7]//LayeredGraphPlot
>
> Also, it is easy to prove that
>
> x --> {4 x + 1, 2 x + 1}
>
> is not confluent, and its graph is tree-like:
>
> NestGraph[{4*#+1, 2*#+1} &, 1, 7]//LayeredGraphPlot
>
> The problem arises when we consider the system
>
> x --> {3 x + 1, 2 x + 1}
>
> which has a resolution of some critical pairs, e.g.,
>
> 3 --> 7 --> 15 --> 31
>
> and
>
> 3 --> 10 --> 31
>
> but other critical pairs like
>
> 4 --> 9
>
> and
>
> 4 --> 13
>
> seems to be impossible to resolve according to the computational evidence.
>
> I wonder if there is a general method to decide the confluence in the
> class of rewriting systems x --> {a x + b, c x + d} as a function of
> the coefficients (a, b, c, d). If this problem turns out undecidable,
> I guess that the proof should be similar to Conway's proof of the
> undecidability of the generalized 3x+1 problem [3], i.e., transforming
> this problem into a universal Turing machine and applying the
> undecidability of the Halting problem.
>
> Kind regards,
> José M.
>
>
> References:
> [1] Church, Alonzo; Rosser, J. Barkley (May 1936), "Some properties of
> conversion", Transactions of the American Mathematical Society, 39
> (3): 472–482, doi:10.2307/1989762, JSTOR 1989762.
>
> [2] Matsumoto, Hideya (1964), "Générateurs et relations des groupes de
> Weyl généralisés", C. R. Acad. Sci. Paris, 258: 3419–3422, MR 0183818
>
> [3] Conway, John H. (1987). "FRACTRAN: A simple universal programming
> language for arithmetic". Open Problems in Communication and
> Computation. Springer-Verlag New York, Inc.: 4–26.
> doi:10.1007/978-1-4612-4808-8_2. ISBN 978-1-4612-9162-6.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211012/b0fba8b2/attachment-0001.html>
More information about the FOM
mailing list