Confluence in number-theoretic rewriting systems

[Frédéric Blanqui]

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>