Proprietatea Church-Rosser
În informatică teoretică și logică matematică , proprietatea Church-Rosser este o proprietate a sistemelor de rescriere . Acesta poartă numele matematicienilor Biserica Alonzo și John Barkley Rosser .
Definiție
Să fie un rescrierea sistem , și să notăm relația de reducere, de închidere reflexiv tranzitive , și în cele din urmă sa reflexivă, tranzitivă și închidere simetrică .
R{\ displaystyle R}
→R{\ displaystyle \ rightarrow _ {R}}
→R∗{\ displaystyle \ rightarrow _ {R} ^ {*}}
⟷R∗{\ displaystyle \ longleftrightarrow _ {R} ^ {*}}![\ longleftrightarrow _ {R} ^ {*}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1bf49a757cff471a853dbe1ba155e8940e6cdf9f)
Spunem că are proprietatea Church-Rosser dacă, pentru orice pereche de termeni precum , există un termen precum și .
R{\ displaystyle R}
M1,M2{\ displaystyle M_ {1}, M_ {2}}
M1⟷R∗M2{\ displaystyle M_ {1} \ longleftrightarrow _ {R} ^ {*} M_ {2}}
M{\ displaystyle M}
M1→R∗M{\ displaystyle M_ {1} \ rightarrow _ {R} ^ {*} M}
M2→R∗M{\ displaystyle M_ {2} \ rightarrow _ {R} ^ {*} M}![M_ {2} \ rightarrow _ {R} ^ {*} M](https://wikimedia.org/api/rest_v1/media/math/render/svg/99f4e3935ce628a6fd59099bb0ce82f07ce0fa14)
Teorema Bisericii-Rosser
Teorema Bisericii-Rosser este un rezultat al calculului lambda . Se afirmă că reducerea beta deține proprietatea Church-Rosser.
Această teoremă a fost stabilită de Church și Rosser în 1936. Rezultatul este valabil în diferite variații și extensii ale lambda-calculului.
Exemplu de aplicare
Pentru sistemele de rescriere, proprietatea Church-Rosser este echivalentă cu proprietatea de confluență , un concept de importanță primară în teoria bazelor lui Gröbner (în special în definiția acestor baze).
Note și referințe
-
Krivine 1993 , p. 18 și următorii.
-
Rougemont și Lassaigne 1993 , Capitolul 9.2: „Reducere și formă normală”, pagina 191.
-
(în) Alonzo Church și J. Barkley Rosser , „ Some Properties of conversion ” , Transactions of the American Mathematical Society , vol. 39, n o 3,Mai 1936, p. 472-482 ( JSTOR 1989762 ).
Bibliografie
-
Jean-Louis Krivine , Lambda-calcul, tipuri și modele , Paris, Masson,1990. Traducere în engleză: Lambda-calculus, tipuri și modele , Ellis Horwood,1993( citește online ).
-
Michel de Rougemont si Richard Lassaigne , logica și bazele informaticii: Logic 1 st ordine, calculabilitate și calculul lambda , Paris, Hermes,1993, viii-248 p. ( ISBN 2-86601-496-0 , zbMATH 0863.03004 , SUDOC 003003825 ).
-
Michel de Rougemont și Richard Lassaigne , Logică și complexitate , Springer-Verlag , col. „Matematică discretă și informatică teoretică”,2003, 361 p. ( ISBN 978-1-85233-565-6 , zbMATH 1083.03001 ).
Articole similare
linkuri externe
<img src="https://fr.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">