The Church–Rosser theorem states that if there are two distinct reductions starting from the same lambda calculus term, then there exists a term that is reachable via a (possibly empty) sequence of reductions from both reducts. Viewing the lambda calculus as an abstract rewriting system, the Church–Rosser theorem is a proof of confluence. As a consequence of the theorem, a term in the lambda calculus has at most one normal form, justifying reference to "the normal form" of a certain term.

PropertyValue
dbpprop:abstract
  • The Church–Rosser theorem states that if there are two distinct reductions starting from the same lambda calculus term, then there exists a term that is reachable via a (possibly empty) sequence of reductions from both reducts. Viewing the lambda calculus as an abstract rewriting system, the Church–Rosser theorem is a proof of confluence. As a consequence of the theorem, a term in the lambda calculus has at most one normal form, justifying reference to "the normal form" of a certain term. The theorem was proved in 1936 by Alonzo Church and J. Barkley Rosser. The Church–Rosser theorem also holds for many variants of the lambda calculus, such as the simply-typed lambda calculus, many calculi with advanced type systems, and Gordon Plotkin's beta-value calculus. Plotkin also used a Church–Rosser theorem to prove that the evaluation of functional programs is a function from programs to values (a subset of the lambda terms).
  • Das Church-Rosser-Theorem ist ein Satz aus der Berechenbarkeitstheorie. Es besagt, dass, wenn zwei Terme s und t konversionsäquivalent (bis auf Umbenennung von gebundenen Variablen gleich) sind und für die es eine Reduktion nach s' und t' gibt, dass diese Redukte s' und t' dann zueinander konfluenzäquivalent sind. Interpretiert man das Lambda-Kalkül als Termersetzungssystem, dann ist das Church-Rosser-Theorem ein Beweis für die Konfluenz im Lambda-Kalkül. Auf der Menge aller Termersetzungssysteme ist Konfluenz unentscheidbar. Als Konsequenz folgt aus dem Church-Rosser-Theorem, dass jeder Term im Lambda-Kalkül mindestens eine Normalordnungsreduktion besitzt.
  • On dit que <math>R</math> a la propriété de Church-Rosser si pour tous les termes <math>M_1, M_2</math> tels que <math>M_1 \leftrightarrow_R^* M_2</math>, il existe un terme <math>M'</math> tel que <math>M_1 \rightarrow_R^* M'</math> et <math>M_2 \rightarrow_R^* M'</math>. Cette propriété est équivalente à la propriété de confluence, notion de premier ordre dans la théorie des bases de Gröbner (en particulier dans la définition même de ces bases).
  • Twierdzenie Churcha-Rossera, to twierdzenie mówiące o tym że rachunek lambda jest silnie konfluentny. Zobacz też: przegląd zagadnień z zakresu matematyki
  • O Teorema de Church-Rosser é um resultado de confluência para o cálculo lambda e também uma propriedade sobre sistemas de redução abstratos equivalente à confluência e a semi-confluência. (Se busca pela propriedade de Church-Rosser consulte confluência em sistemas de reescrita de termos.)
dbpprop:hasPhotoCollection
dbpprop:reference
rdf:type
rdfs:comment
  • The Church–Rosser theorem states that if there are two distinct reductions starting from the same lambda calculus term, then there exists a term that is reachable via a (possibly empty) sequence of reductions from both reducts. Viewing the lambda calculus as an abstract rewriting system, the Church–Rosser theorem is a proof of confluence. As a consequence of the theorem, a term in the lambda calculus has at most one normal form, justifying reference to "the normal form" of a certain term.
  • Das Church-Rosser-Theorem ist ein Satz aus der Berechenbarkeitstheorie. Es besagt, dass, wenn zwei Terme s und t konversionsäquivalent (bis auf Umbenennung von gebundenen Variablen gleich) sind und für die es eine Reduktion nach s' und t' gibt, dass diese Redukte s' und t' dann zueinander konfluenzäquivalent sind. Interpretiert man das Lambda-Kalkül als Termersetzungssystem, dann ist das Church-Rosser-Theorem ein Beweis für die Konfluenz im Lambda-Kalkül.
  • On dit que <math>R</math> a la propriété de Church-Rosser si pour tous les termes <math>M_1, M_2</math> tels que <math>M_1 \leftrightarrow_R^* M_2</math>, il existe un terme <math>M'</math> tel que <math>M_1 \rightarrow_R^* M'</math> et <math>M_2 \rightarrow_R^* M'</math>.
  • Twierdzenie Churcha-Rossera, to twierdzenie mówiące o tym że rachunek lambda jest silnie konfluentny. Zobacz też: przegląd zagadnień z zakresu matematyki
  • O Teorema de Church-Rosser é um resultado de confluência para o cálculo lambda e também uma propriedade sobre sistemas de redução abstratos equivalente à confluência e a semi-confluência. (Se busca pela propriedade de Church-Rosser consulte confluência em sistemas de reescrita de termos.)
rdfs:label
  • Church–Rosser theorem
  • Church-Rosser-Theorem
  • Propriété de Church-Rosser
  • Twierdzenie Churcha-Rossera
  • Teorema de Church-Rosser
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of
is owl:sameAs of