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.
| Attributes | Values |
|---|
| rdf:type
| |
| 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)
|
| 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)
|
| foaf:depiction
| |
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| thumbnail
| |
| has 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)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage redirect
of | |
| is known for
of | |
| is known for
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)
