Church–Rosser theorem (original) (raw)
Das Church-Rosser-Theorem (bewiesen im Jahr 1936 von Alonzo Church und John Barkley Rosser) ist ein wichtiges Resultat aus der Theorie des Lambda-Kalküls. Eine Konsequenz dieses Theorems ist, dass jeder Term des Lambda-Kalküls höchstens eine Normalform besitzt. Das Church-Rosser-Theorem lässt Verallgemeinerungen auf abstrakte Reduktionssysteme zu.
| Property | Value |
|---|---|
| dbo:abstract | Das Church-Rosser-Theorem (bewiesen im Jahr 1936 von Alonzo Church und John Barkley Rosser) ist ein wichtiges Resultat aus der Theorie des Lambda-Kalküls. Eine Konsequenz dieses Theorems ist, dass jeder Term des Lambda-Kalküls höchstens eine Normalform besitzt. Das Church-Rosser-Theorem lässt Verallgemeinerungen auf abstrakte Reduktionssysteme zu. (de) In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result. More precisely, if there are two distinct reductions or sequences of reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying (possibly empty) sequences of additional reductions. The theorem was proved in 1936 by Alonzo Church and J. Barkley Rosser, after whom it is named. The theorem is symbolized by the adjacent diagram: If term a can be reduced to both b and c, then there must be a further term d (possibly equal to either b or c) to which both b and c can be reduced.Viewing the lambda calculus as an abstract rewriting system, the Church–Rosser theorem states that the reduction rules of the lambda calculus are confluent. 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 given normalizable term. (en) En informatique théorique et en logique mathématique, la propriété de Church-Rosser est une propriété des systèmes de réécriture. Elle est nommée ainsi d'après les mathématiciens Alonzo Church et John Barkley Rosser. (fr) 처치-로서 정리는 두 개의 특별한 재작성이 동일한 람다 대수항으로부터 시작한다면, 해당 항으로부터 재작성을 거듭하면 결국 어느 하나의 항 표현에 도달한다는 사실을 주장한다. 이는 우측의 그림으로 도식화되어 있다. a 항이 b와 c로 재작성가능하다면, d(이는 근본적으로 b랑 c와 동일하다)는 b와 c로 재작성 가능하다. 추상 재작성 시스템 상에서의 람다 대수 상에서 처치-로서 정리는 합류성 정리이기도 하다. 정리를 거듭해보면 람다 대수의 한 항은 최소한 하나의 을 가지게 되어 있다. 이는 해당 표준 형식의 특정 형태라는 걸 증명함으로써 가능하다. 이 정리는 알론조 처치와 존 버클리 로서에 의해 1936년 증명되었다. 처치-로서 정리는 또한 람다 대수의 많은 변형을 가져오는데, 단순한 타입 기반 람다 대수(simply-typed lambda calculus), 고급 타입 시스템의 기초가 되는 수많은 정리, 그리고 고든 프로킨(Gordon Plotkin)의 베타-값 대수와 같은 것이 있다. 프로킨은 처치-로서 정리를 필요한 대로의 계산(lazy evaluation)이나 성급한 계산(eager evaluation)과 같은 함수형 프로그래밍 기법의 계산 방식이 람다 대수를 통해 가능함을 증명하는데 사용하기도 하였다. (ko) チャーチ・ロッサーの定理（チャーチ・ロッサーのていり、英: Church–Rosser theorem）とは、同じラムダ式から始まる二個の異なる簡約がある場合、それぞれの簡約から一連の簡約を行うことで到達可能な式があることを述べる定理である。詳しくは合流性を参照。 (ja) Теорема Чёрча — Россера — одна из основных теорем лямбда-исчисления, утверждающая что порядок применения правил редукции к термам не влияет на конечный результат. Точнее, при наличии двух различных редукций или последовательностей редукций, которые могут быть применены к одному и тому же терму, всегда существует терм, достижимый из результатов обеих редукций применением (возможно, пустых) последовательностей дополнительных редукций. Теорема была доказана в 1936 году Алонзо Черчем и , в честь которых она названа. (ru) 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.) (pt) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Confluence.svg?width=300 |
| dbo:wikiPageExternalLink | ftp://ftp.cs.ru.nl/pub/CompMath.Found/ErrataLCalculus.pdf http://www.elsevier.com/wps/find/bookdescription.cws_home/501727/description https://web.archive.org/web/20040823174002/https:/www.elsevier.com/wps/find/bookdescription.cws_home/501727/description http://www.ams.org/tran/1936-039-03/S0002-9947-1936-1501858-0/S0002-9947-1936-1501858-0.pdf%7Cdoi-access=free https://plato.stanford.edu/archives/fall2017/entries/lambda-calculus/%7Ctitle=The |
| dbo:wikiPageID | 150035 (xsd:integer) |
| dbo:wikiPageLength | 7887 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1052509544 (xsd:integer) |
| dbo:wikiPageWikiLink | dbc:Lambda_calculus dbr:Beta_normal_form dbr:Per_Martin-Löf dbr:Gordon_Plotkin dbr:Confluence_(abstract_rewriting) dbr:Simply_typed_lambda_calculus dbr:Type_system dbr:Eager_evaluation dbr:Lazy_evaluation dbr:Alonzo_Church dbc:Theorems_in_the_foundations_of_mathematics dbr:J._Barkley_Rosser dbr:Term_(logic) dbr:Abstract_rewriting_system dbc:Rewriting_systems dbr:Lambda_calculus dbr:Newman's_lemma dbr:William_W._Tait dbr:Subset dbr:Transactions_of_the_American_Mathematical_Society dbr:Functional_program dbr:File:Confluence.svg |
| dbp:wikiPageUsesTemplate | dbt:Citation dbt:Cite_book dbt:Reflist dbt:Sfnp |
| dcterms:subject | dbc:Lambda_calculus dbc:Theorems_in_the_foundations_of_mathematics dbc:Rewriting_systems |
| rdf:type | yago:WikicatMathematicalTheorems yago:WikicatTheoremsInTheFoundationsOfMathematics yago:Abstraction100002137 yago:Communication100033020 yago:Message106598915 yago:Proposition106750804 yago:Statement106722453 yago:Theorem106752293 |
| rdfs:comment | Das Church-Rosser-Theorem (bewiesen im Jahr 1936 von Alonzo Church und John Barkley Rosser) ist ein wichtiges Resultat aus der Theorie des Lambda-Kalküls. Eine Konsequenz dieses Theorems ist, dass jeder Term des Lambda-Kalküls höchstens eine Normalform besitzt. Das Church-Rosser-Theorem lässt Verallgemeinerungen auf abstrakte Reduktionssysteme zu. (de) En informatique théorique et en logique mathématique, la propriété de Church-Rosser est une propriété des systèmes de réécriture. Elle est nommée ainsi d'après les mathématiciens Alonzo Church et John Barkley Rosser. (fr) チャーチ・ロッサーの定理（チャーチ・ロッサーのていり、英: Church–Rosser theorem）とは、同じラムダ式から始まる二個の異なる簡約がある場合、それぞれの簡約から一連の簡約を行うことで到達可能な式があることを述べる定理である。詳しくは合流性を参照。 (ja) Теорема Чёрча — Россера — одна из основных теорем лямбда-исчисления, утверждающая что порядок применения правил редукции к термам не влияет на конечный результат. Точнее, при наличии двух различных редукций или последовательностей редукций, которые могут быть применены к одному и тому же терму, всегда существует терм, достижимый из результатов обеих редукций применением (возможно, пустых) последовательностей дополнительных редукций. Теорема была доказана в 1936 году Алонзо Черчем и , в честь которых она названа. (ru) 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.) (pt) In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result. More precisely, if there are two distinct reductions or sequences of reductions that can be applied to the same term, then there exists a term that is reachable from both results, by applying (possibly empty) sequences of additional reductions. The theorem was proved in 1936 by Alonzo Church and J. Barkley Rosser, after whom it is named. (en) 처치-로서 정리는 두 개의 특별한 재작성이 동일한 람다 대수항으로부터 시작한다면, 해당 항으로부터 재작성을 거듭하면 결국 어느 하나의 항 표현에 도달한다는 사실을 주장한다. 이는 우측의 그림으로 도식화되어 있다. a 항이 b와 c로 재작성가능하다면, d(이는 근본적으로 b랑 c와 동일하다)는 b와 c로 재작성 가능하다. 추상 재작성 시스템 상에서의 람다 대수 상에서 처치-로서 정리는 합류성 정리이기도 하다. 정리를 거듭해보면 람다 대수의 한 항은 최소한 하나의 을 가지게 되어 있다. 이는 해당 표준 형식의 특정 형태라는 걸 증명함으로써 가능하다. 이 정리는 알론조 처치와 존 버클리 로서에 의해 1936년 증명되었다. (ko) |
| rdfs:label | Satz von Church-Rosser (de) Church–Rosser theorem (en) Propriété de Church-Rosser (fr) チャーチ・ロッサーの定理 (ja) 처치-로서 정리 (ko) Teorema de Church-Rosser (pt) Теорема Чёрча — Россера (ru) |
| owl:sameAs | freebase:Church–Rosser theorem wikidata:Church–Rosser theorem dbpedia-de:Church–Rosser theorem dbpedia-fr:Church–Rosser theorem dbpedia-hr:Church–Rosser theorem dbpedia-ja:Church–Rosser theorem dbpedia-ko:Church–Rosser theorem dbpedia-pt:Church–Rosser theorem dbpedia-ru:Church–Rosser theorem dbpedia-vi:Church–Rosser theorem https://global.dbpedia.org/id/L5nF |
| prov:wasDerivedFrom | wikipedia-en:Church–Rosser_theorem?oldid=1052509544&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Confluence.svg |
| foaf:isPrimaryTopicOf | wikipedia-en:Church–Rosser_theorem |
| is dbo:knownFor of | dbr:Alonzo_Church dbr:J._Barkley_Rosser |
| is dbo:wikiPageRedirects of | dbr:Church-Rosser_theorem dbr:Church-Rosser |
| is dbo:wikiPageWikiLink of | dbr:List_of_functional_programming_topics dbr:Deductive_lambda_calculus dbr:List_of_mathematical_logic_topics dbr:Sahlqvist_formula dbr:Confluence_(abstract_rewriting) dbr:Stephen_Wolfram dbr:Alonzo_Church dbr:J._Barkley_Rosser dbr:Lambda_calculus dbr:Church-Rosser_theorem dbr:List_of_theorems dbr:Church-Rosser |
| is dbp:knownFor of | dbr:Alonzo_Church dbr:J._Barkley_Rosser |
| is foaf:primaryTopic of | wikipedia-en:Church–Rosser_theorem |
