Church encoding (original) (raw)
Unter Church-Kodierung versteht man die Einbettung von Daten und Operatoren in den Lambda-Kalkül. Die bekannteste Form sind die Church-Numerale, welche die natürlichen Zahlen repräsentieren. Benannt sind sie nach Alonzo Church, der Daten als Erster auf diese Weise modellierte.
Property | Value |
---|---|
dbo:abstract | Στα μαθηματικά η κωδικοποίηση Τσερτς (Αγγλικά: Church encoding) είναι ένα μέσο αναπαράστασης δεδομένων και τελεστών με λάμδα-λογισμό (συμβολίζεται ως λ-λογισμός ή στα αγγλικά: λ-calculus). Τα δεδομένα και οι τελεστές δημιουργούν μια μαθηματική δομή η οποία ενσωματώνεται στον λ-λογισμό. Τα αριθμοειδή Τσερτς (ή και αριθμιακά Τσερτς, στα Αγγλικά: Church numerals) είναι αναπαραστάσεις των φυσικών αριθμών χρησιμοποιώντας λάμδα συμβολισμούς. Οι αναπαραστάσεις αυτές έχουν πάρει από το όνομα του Αλόνζο Τσερτς ο οποίος πρώτη φορά κωδικοποίησε δεδομένα με αυτή τη μορφή (χρησιμοποιώντας λ-λογισμό). Οι όροι συνήθως θεωρούνται πρωτογενείς (Αγγλικά: primitive) σε διαφορετική αναπαράσταση (όπως ακέραιοι, λογικοί τύποι, ζεύγη ή λίστες) και αντιστοιχίζονται σε συναρτήσεις ανώτερου βαθμού (Αγγλικά: high order functions) κάτω από την κωδικοποίηση Τσερτς. Σύμφωνα με την θέση Τσερτς-Τούρνινγκ αποδεικνύεται ότι κάθε υπολογίσιμος τελεστής (και οι παράμετροί του) μπορούν να αναπαρασταθούν με την κωδικοποίηση του Τσερτς. Στον λ-λογισμό χωρίς τύπους ο μόνος πρωτογενής τύπος είναι η συνάρτηση. (el) Unter Church-Kodierung versteht man die Einbettung von Daten und Operatoren in den Lambda-Kalkül. Die bekannteste Form sind die Church-Numerale, welche die natürlichen Zahlen repräsentieren. Benannt sind sie nach Alonzo Church, der Daten als Erster auf diese Weise modellierte. (de) In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way. Terms that are usually considered primitive in other notations (such as integers, booleans, pairs, lists, and tagged unions) are mapped to higher-order functions under Church encoding. The Church-Turing thesis asserts that any computable operator (and its operands) can be represented under Church encoding. In the untyped lambda calculus the only primitive data type is the function. (en) In informatica, un booleano di Church è una funzione concettuale che prende in considerazione due parametri di valutazione lazy (come i blocchi o i lambda) e valuta o l'uno o l'altro. Il concetto prende il nome da Alonzo Church, inventore del lambda calcolo. Ci sono solo due booleani di Church: vero e falso. Alcuni linguaggi di programmazione li usano come modello di implementazione per l'aritmetica booleana: esempi ne sono Smalltalk e Pico. Definizione formale nel lambda calcolo: * vero=λab.a * falso=λab.b (it) Liczby naturalne Churcha – konstrukcja w rachunku lambda, umożliwiająca wykonywanie normalnej arytmetyki. Rachunek lambda bez typów nie zawiera sam z siebie liczb, więc należy je skonstruować. Liczba naturalna Churcha to funkcja wyższego rzędu pobierająca dwa argumenty – funkcję i argument która -krotnie aplikuje do Tak więc w zapisie matematycznym: * 0 to * 1 to * 2 to * 3 to * N+1 to a w zapisie lambda: liczba naturalna to gdzie: to to Operacje na liczbach naturalnych Churcha są opisane w artykule arytmetyka w rachunku lambda. (pl) Em matemática, a codificação de Church é uma forma de incorporar dados e operadores ao cálculo lambda, a forma mais conhecida dos numerais de Church, uma representação dos números naturais usando a notação lambda. O método é conhecido como Alonzo Church, que foi o primeiro a codificar os dados no cálculo lambda desta forma. Termos que são geralmente considerados primitivos em outras notações (com inteiros, booleanos e pares, por exemplo) são mapeados para funções de ordem superior na codificação de Church. A tese de Church-Turing afirma que qualquer operador computável (e seus operandos) pode ser representado sob a codificação de Church. Muitos estudantes de matemática estão familiarizados com a numeração de Gödel de elementos de um conjunto. A codificação de Church é uma operação equivalente, definida sob lambda-abstrações, o invés de números naurais. (pt) В математике кодирование Чёрча означает представление (или процедуру представления) данных и операторов в процедуре лямбда-исчисления. Необходимость процедуры вызвана тем, что в чистом лямбда-исчислении среди термов присутствуют только переменные и отсутствуют константы. Для того, чтобы получить объекты, ведущие себя таким же образом как и числа, применяется кодирование Чёрча. Сама процедура названа в честь Алонзо Чёрча, разработавшего лямбда-исчисление и впервые применившего этот метод кодирования данных. По аналогии с числами, кодирование Чёрча может быть применено и для представления объектов других типов, ведущих себя как константы. Термы, которые в других нотациях обычно являются примитивами (такие как целые числа, логические значения, пары, списки и теговые объединения), в кодировке Черча представляются при помощи функций высшего порядка. В одной из своих формулировок тезис Тьюринга - Чёрча утверждает, что в кодировке Чёрча может быть представлен любой вычислимый оператор (и его операнды). В бестиповом лямбда-исчислении единственным примитивным типом данных являются функции, а все остальные сущности конструируются при помощи кодирования Чёрча. Кодировка Черча, как правило, не используется для практической реализации примитивных типов данных. Она используется для целей доказательной демонстрации того, что для проведения вычислений другие примитивные типы данных не обязательны. (ru) 邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式,最常见的形式即邱奇数,它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇,他首先以这种方法把数据编码到lambda演算中。 透過邱奇編碼,在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和tagged unions)都會被映射到高阶函数。在無型別lambda演算,函數是唯一的原始型別。 邱奇編碼本身並非用來實踐原始型別,而是透過它來展現我們不須額外原始型別即可表達計算。 很多学数学的学生熟悉可计算函数集合的哥德尔编号;邱奇编码是定义在lambda抽象而不是自然数上的等价运算。 (zh) |
dbo:wikiPageExternalLink | http://blog.klipse.tech/lambda/2016/07/24/lambda-calculus-2.html http://www.cs.uiowa.edu/~astump/papers/archon.pdf http://www.cs.rice.edu/~javaplt/311/Readings/supplemental.pdf https://espace.library.uq.edu.au/view/UQ:171001 http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/const-int/ |
dbo:wikiPageID | 2989409 (xsd:integer) |
dbo:wikiPageLength | 40926 (xsd:nonNegativeInteger) |
dbo:wikiPageRevisionID | 1122831184 (xsd:integer) |
dbo:wikiPageWikiLink | dbr:Scala_(programming_language) dbr:Monus dbr:Beta_reduction dbc:Lambda_calculus dbr:Rice_University dbr:Deductive_lambda_calculus dbr:Mathematics dbr:Function_composition dbr:Multiplication dbr:Cons dbr:Continuation dbr:Ostensive_definition dbr:Smalltalk dbr:Computable_number dbr:Functional_programming dbr:Subtraction dbr:Successor_function dbr:Turing_complete dbr:Truth_value dbr:Lambda_lifting dbr:Addition dbr:Algebraic_data_type dbr:Alonzo_Church dbr:Exponentiation dbr:Church-Turing_thesis dbr:Fold_(higher-order_function) dbr:Haskell_(programming_language) dbr:Higher-order_function dbr:Arithmetic dbr:Lambda_calculus dbr:Mogensen–Scott_encoding dbr:System_F dbr:Division_(mathematics) dbr:Pico_(programming_language) dbr:Integer dbr:Natural_number dbr:Ordinal_number dbr:Church's_theorem dbr:Extensionality dbr:Immutable_object dbr:Fixed-point_combinator dbr:List_(computing) dbr:Higher-ranked_type |
dbp:date | March 2022 (en) December 2019 (en) |
dbp:reason | The Church-Turing thesis is that lambda calculus is Turing complete. (en) |
dbp:wikiPageUsesTemplate | dbt:Cite_journal dbt:Cite_thesis dbt:Cite_web dbt:Clarification_needed dbt:Dubious dbt:Math dbt:Mvar dbt:See_also dbt:Short_description dbt:Mathematical_logic |
dct:subject | dbc:Lambda_calculus |
gold:hypernym | dbr:Means |
rdf:type | owl:Thing dbo:Software |
rdfs:comment | Unter Church-Kodierung versteht man die Einbettung von Daten und Operatoren in den Lambda-Kalkül. Die bekannteste Form sind die Church-Numerale, welche die natürlichen Zahlen repräsentieren. Benannt sind sie nach Alonzo Church, der Daten als Erster auf diese Weise modellierte. (de) In informatica, un booleano di Church è una funzione concettuale che prende in considerazione due parametri di valutazione lazy (come i blocchi o i lambda) e valuta o l'uno o l'altro. Il concetto prende il nome da Alonzo Church, inventore del lambda calcolo. Ci sono solo due booleani di Church: vero e falso. Alcuni linguaggi di programmazione li usano come modello di implementazione per l'aritmetica booleana: esempi ne sono Smalltalk e Pico. Definizione formale nel lambda calcolo: * vero=λab.a * falso=λab.b (it) Liczby naturalne Churcha – konstrukcja w rachunku lambda, umożliwiająca wykonywanie normalnej arytmetyki. Rachunek lambda bez typów nie zawiera sam z siebie liczb, więc należy je skonstruować. Liczba naturalna Churcha to funkcja wyższego rzędu pobierająca dwa argumenty – funkcję i argument która -krotnie aplikuje do Tak więc w zapisie matematycznym: * 0 to * 1 to * 2 to * 3 to * N+1 to a w zapisie lambda: liczba naturalna to gdzie: to to Operacje na liczbach naturalnych Churcha są opisane w artykule arytmetyka w rachunku lambda. (pl) 邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式,最常见的形式即邱奇数,它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇,他首先以这种方法把数据编码到lambda演算中。 透過邱奇編碼,在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和tagged unions)都會被映射到高阶函数。在無型別lambda演算,函數是唯一的原始型別。 邱奇編碼本身並非用來實踐原始型別,而是透過它來展現我們不須額外原始型別即可表達計算。 很多学数学的学生熟悉可计算函数集合的哥德尔编号;邱奇编码是定义在lambda抽象而不是自然数上的等价运算。 (zh) Στα μαθηματικά η κωδικοποίηση Τσερτς (Αγγλικά: Church encoding) είναι ένα μέσο αναπαράστασης δεδομένων και τελεστών με λάμδα-λογισμό (συμβολίζεται ως λ-λογισμός ή στα αγγλικά: λ-calculus). Τα δεδομένα και οι τελεστές δημιουργούν μια μαθηματική δομή η οποία ενσωματώνεται στον λ-λογισμό. Τα αριθμοειδή Τσερτς (ή και αριθμιακά Τσερτς, στα Αγγλικά: Church numerals) είναι αναπαραστάσεις των φυσικών αριθμών χρησιμοποιώντας λάμδα συμβολισμούς. Οι αναπαραστάσεις αυτές έχουν πάρει από το όνομα του Αλόνζο Τσερτς ο οποίος πρώτη φορά κωδικοποίησε δεδομένα με αυτή τη μορφή (χρησιμοποιώντας λ-λογισμό). (el) In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way. (en) Em matemática, a codificação de Church é uma forma de incorporar dados e operadores ao cálculo lambda, a forma mais conhecida dos numerais de Church, uma representação dos números naturais usando a notação lambda. O método é conhecido como Alonzo Church, que foi o primeiro a codificar os dados no cálculo lambda desta forma. Termos que são geralmente considerados primitivos em outras notações (com inteiros, booleanos e pares, por exemplo) são mapeados para funções de ordem superior na codificação de Church. A tese de Church-Turing afirma que qualquer operador computável (e seus operandos) pode ser representado sob a codificação de Church. Muitos estudantes de matemática estão familiarizados com a numeração de Gödel de elementos de um conjunto. A codificação de Church é uma operação equivale (pt) В математике кодирование Чёрча означает представление (или процедуру представления) данных и операторов в процедуре лямбда-исчисления. Необходимость процедуры вызвана тем, что в чистом лямбда-исчислении среди термов присутствуют только переменные и отсутствуют константы. Для того, чтобы получить объекты, ведущие себя таким же образом как и числа, применяется кодирование Чёрча. Сама процедура названа в честь Алонзо Чёрча, разработавшего лямбда-исчисление и впервые применившего этот метод кодирования данных. По аналогии с числами, кодирование Чёрча может быть применено и для представления объектов других типов, ведущих себя как константы. (ru) |
rdfs:label | Church-Kodierung (de) Κωδικοποίηση Τσερτς (el) Church encoding (en) Booleano di Church (it) Liczby naturalne Churcha (pl) Codificação de Church (pt) Кодирование Чёрча (ru) 邱奇数 (zh) |
rdfs:seeAlso | dbr:Cons |
owl:sameAs | freebase:Church encoding wikidata:Church encoding dbpedia-de:Church encoding dbpedia-el:Church encoding dbpedia-fa:Church encoding dbpedia-it:Church encoding dbpedia-pl:Church encoding dbpedia-pt:Church encoding dbpedia-ru:Church encoding dbpedia-zh:Church encoding https://global.dbpedia.org/id/AJRM |
prov:wasDerivedFrom | wikipedia-en:Church_encoding?oldid=1122831184&ns=0 |
foaf:isPrimaryTopicOf | wikipedia-en:Church_encoding |
is dbo:knownFor of | dbr:Alonzo_Church |
is dbo:wikiPageRedirects of | dbr:Church_boolean dbr:Church_booleans dbr:Church_integer dbr:Church_number dbr:Church_numbers dbr:Church_numeral dbr:Church_numerals |
is dbo:wikiPageWikiLink of | dbr:Deductive_lambda_calculus dbr:Combinatory_logic dbr:Cons dbr:Calculus_of_constructions dbr:Simply_typed_lambda_calculus dbr:Type_theory dbr:Gödel_numbering dbr:Alonzo_Church dbr:Unary_numeral_system dbr:Lambda_calculus dbr:Mogensen–Scott_encoding dbr:System_F dbr:OCaml dbr:Visitor_pattern dbr:Fixed-point_combinator dbr:Parametricity dbr:Church_boolean dbr:Church_booleans dbr:Church_integer dbr:Church_number dbr:Church_numbers dbr:Church_numeral dbr:Church_numerals |
is dbp:knownFor of | dbr:Alonzo_Church |
is foaf:primaryTopic of | wikipedia-en:Church_encoding |