Propriedade Church-Rosser

Na ciência da computação teórica e na lógica matemática , a propriedade Church-Rosser é uma propriedade de sistemas de reescrita . Recebeu o nome dos matemáticos Alonzo Church e John Barkley Rosser .

Definição

Deixe ser um sistema de reescrita , e vamos denotar a relação de redução, seu fechamento reflexivo transitivo e, finalmente, seu fechamento reflexivo, transitivo e simétrico . $R$ $\ rightarrow _ {R}$ $\ rightarrow _ {R} ^ {*}$ $\ longleftrightarrow _ {R} ^ {*}$

Dizemos que tem a propriedade Church-Rosser se, para qualquer par de termos como , existe um termo como e . $R$ $M_ {1}, M_ {2}$ $M_ {1} \ longleftrightarrow _ {R} ^ {*} M_ {2}$ $M$ $M_ {1} \ rightarrow _ {R} ^ {*} M$ $M_ {2} \ rightarrow _ {R} ^ {*} M$

Teorema de Church-Rosser

O teorema de Church-Rosser é o resultado do cálculo lambda . Afirma que a redução beta possui a propriedade de Church-Rosser.

Este teorema foi estabelecido por Church e Rosser em 1936. O resultado é verdadeiro em várias variações e extensões do cálculo lambda.

Exemplo de aplicação

Para sistemas de reescrita, a propriedade Church-Rosser é equivalente à propriedade confluência , um conceito de importância primária na teoria das bases de Gröbner (em particular na própria definição dessas bases).

Notas e referências

Krivine 1993 , p. 18 e seguintes.
Rougemont e Lassaigne 1993 , Capítulo 9.2: “Redução e forma normal”, página 191.
(em) Alonzo Church e J. Barkley Rosser , " Some Properties of conversion " , Transactions of the American Mathematical Society , vol. 39, n o 3,Maio de 1936, p. 472-482 ( JSTOR 1989762 ).

Bibliografia

Jean-Louis Krivine , Lambda-calcul, types and models , Paris, Masson,1990. Tradução para o inglês: Lambda-calculus, types and models , Ellis Horwood,1993( leia online ).
Michel de Rougemont e Richard Lassaigne , Lógica e fundamentos da ciência da computação: Lógica 1 st fim, computability e cálculo lambda , Paris, Hermes,1993, viii-248 p. ( ISBN 2-86601-496-0 , zbMATH 0.863,03004 , SUDOC 003003825 ).
Michel de Rougemont e Richard Lassaigne , Lógica e complexidade , Springer-Verlag , col. "Matemática Discreta e Ciência da Computação Teórica",2003, 361 p. ( ISBN 978-1-85233-565-6 , zbMATH 1083.03001 ).

links externos

(en) Eric W. Weisstein , “ Church-Rosser-Theorem ” , no MathWorld