Combinatory logic (original) (raw)
Kombinatorische Logik (Abgekürzt CL für engl. Combinatory Logic) ist eine Notation, die von Moses Schönfinkel und Haskell Brooks Curry eingeführt wurde, um die Verwendung von Variablen in der Mathematischen Logik zu vermeiden. Sie wird besonders in der Informatik als theoretisches Modell für Berechnung, als auch als Grundlage zum Design funktionaler Programmiersprachen eingesetzt.
| Property | Value | |
|---|---|---|
| dbo:abstract | La lògica combinatòria és la lògica última i com a tal pot ser un model simplificat del còmput, usat en la teoria de computabilitat (l'estudi de què pot ser computat) i la teoria de la prova (l'estudi de què es pot provar matemàticament). La teoria, a causa de la seva simplicitat, captura les característiques essencials de la naturalesa del còmput. La lògica combinatòria (LC) és el fonament del càlcul lambda, en eliminar el darrer tipus de variable d'aquest: la variable lambda. En LC les expressions lambda (usades per permetre l'abstracció funcional), són substituïdes per un sistema limitat de combinacions, les funcions primitives que no contenen cap ( ni lligada). És fàcil transformar expressions lambda en expressions combinatòries, i ja que la reducció d'un combinat és més simple que la reducció lambda, LC s'ha utilitzat com a base per a la posada en pràctica d'alguns llenguatges de programació funcionals no estrictes en programari i maquinari. (ca) Kombinatorische Logik (Abgekürzt CL für engl. Combinatory Logic) ist eine Notation, die von Moses Schönfinkel und Haskell Brooks Curry eingeführt wurde, um die Verwendung von Variablen in der Mathematischen Logik zu vermeiden. Sie wird besonders in der Informatik als theoretisches Modell für Berechnung, als auch als Grundlage zum Design funktionaler Programmiersprachen eingesetzt. (de) Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments. (en) La lógica combinatoria es la lógica última y como tal puede ser un modelo simplificado del cómputo, usado en la teoría de la computabilidad (el estudio de qué puede ser computado) y la teoría de la prueba (el estudio de qué se puede probar matemáticamente). (es) En logique mathématique, la logique combinatoire est une théorie logique introduite par Moses Schönfinkel en 1920 lors d'une conférence et développée dès 1929 par Haskell Brooks Curry pour supprimer le besoin de variables en mathématiques, pour formaliser rigoureusement la notion de fonction et pour minimiser le nombre d'opérateurs nécessaires pour définir le calcul des prédicats à la suite de Henry M. Sheffer. Plus récemment, elle a été utilisée en informatique comme modèle théorique de calcul et comme base pour la conception de langages de programmation fonctionnels. Le concept de base de la logique combinatoire est celui de combinateur qui est une fonction d'ordre supérieur ; elle utilise uniquement l'application de fonctions et éventuellement d'autres combinateurs pour définir de nouvelles fonctions d'ordre supérieur. Chaque combinateur simplement typable est une démonstration à la Hilbert en logique intuitionniste et vice-versa . On appelle ceci la correspondance de Curry-Howard (fr) コンビネータ論理（英: combinatory logic、組み合わせ論理）は、（露: Моисей Эльевич Шейнфинкель、英: Moses Ilyich Schönfinkel）とハスケル・カリー（英: Haskell Brooks Curry）によって、記号論理での変数を消去するために導入された記法である。最近では、計算機科学において計算の理論的モデルで利用されてきている。また、関数型プログラミング言語の理論（意味論など）や実装にも応用がある。 コンビネータ論理は、コンビネータまたは引数のみからなる関数適用によって結果が定義されている高階関数、コンビネータに基づいている。 (ja) De combinatorische logica (ook: combinatoire logica) was oorspronkelijk een door en Haskell Curry bedachte notatie in de wiskundige logica, waarmee de noodzakelijkheid van het gebruik van variabelen verdween. De laatste tijd wordt deze notatie vooral gebruikt in de computerwetenschap, meer in het bijzonder in de theoretische informatica en voor het ontwerpen van functionele programmeertalen. De notatie is gebaseerd op combinatoren in de vorm van een hogere-ordefunctie zonder vrije variabelen. (nl) Rachunek kombinatorów (ang. Combinatory Calculi) to jeden z najprostszych możliwych uniwersalnych systemów formalnych. Na język rachunku kombinatorów składają się kombinator stały K, kombinator rozdzielonej aplikacji S, oraz kombinatory aplikacji złożone z pary dowolnych kombinatorów - funkcji i argumentu: * σ = S | K | (σ σ) Derywacją rządzą dwie reguły: * ((K α) β) → α * (((S α) β) γ) → ((α γ) (β γ)) Gdzie α, β i γ to dowolne kombinatory. Tak prosty system jest w stanie wyrazić wszystko, co jest w stanie wyrazić rachunek lambda, dowolna maszyna Turinga czy w ogóle dowolny algorytm. Kombinatory mają prostą interpretację w rachunku lambda: * K = λ x . λ y . x * S = λ x . λ y . λ z . (x z) (y z) Często wprowadza się też kombinator identyczności I z regułą: * (I α) → α Ponieważ system SK już jest kompletny, kombinator ten można przepisać jako (SK)K: * (((S K) K) α) → ((K α) (K α)) → α Podobnie jak w rachunku lambda zwykle pomija się nadmiarowe nawiasy, zakładając wiązanie w lewo: α β γ to więc ((α β) γ). Ponieważ każdy kombinator ma bardzo prostą interpretację w rachunku lambda, badania rachunku kombinatorów są zwykle częścią badań nad rachunkiem lambda. Z zupełności systemu SK wynika, że każde λ wyrażenie bez zmiennych wolnych (w terminologii rachunku lambda również zwane kombinatorem) można zapisać za pomocą S i K, jednak ze względu na uboższy język, takie wyrażenia mają tendencję do przybierania bardzo dużych rozmiarów. (pl) Lógica combinatória é uma notação introduzida por Moses Schönfinkel e Haskell Curry para eliminar a necessidade de variáveis em lógica matemática. Vem sendo mais usada recentemente na ciência da computação como um modelo de computação e como base para o desenvolvimento de linguagens de programação funcionais. Ela é baseada em combinadores, somente usam aplicações de funções e outros combinadores para definir um resultado a partir de seus parâmetros. (pt) Комбина́торная ло́гика — направление математической логики, занимающееся фундаментальными (то есть не нуждающимися в объяснении и не анализируемыми) понятиями и методами формальных логических систем или исчислений. В дискретной математике комбинаторная логика тесно связана с лямбда-исчислением, так как описывает вычислительные процессы. С момента своего возникновения комбинаторная логика и лямбда-исчисление были отнесены к неклассическим логикам. Дело заключается в том, что комбинаторная логика возникла в 1920-х годах, а лямбда-исчисление — в 1940-х годах как ветвь метаматематики с достаточно очерченным предназначением — дать основания математике. Это означает, что сконструировав требуемую «прикладную» математическую теорию — предметную теорию, — которая отражает процессы или явления в реальной внешней среде, можно воспользоваться «чистой» метатеорией как оболочкой для выяснения возможностей и свойств предметной теории. Вскоре также оказалось, что обе эти системы можно рассматривать как языки программирования (см. также комбинаторное программирование). К настоящему времени оба эти языка не только стали основой для всей массы исследований в области информатики, но и широко используются в теории программирования. Рост вычислительной мощности компьютеров привёл к автоматизации значительной части теоретического (логического и математического) знания, а комбинаторная логика вместе с лямбда-исчислением признаются основой для рассуждений в терминах объектов. (ru) 组合子逻辑是和哈斯凱爾·加里介入的一种符号系统，用来消除数理逻辑中对变量的需要。它最近在计算机科学中被用做计算的理论模型和设计函数式编程语言的基础。它所基于的组合子是只使用函数应用或早先定义的组合子来定义从它们的参数得出的结果的高阶函数。 (zh) Комбінаторна логіка — це нотація для усунення необхідності кількісних змінних в математичній логіці. Вона була введена Мойсейем Шейнфінкелем і Гаскеллем Каррі, та використовується в інформатиці як теоретична модель обчислень, а також як основа для розробки функціональних мов програмування. Вона заснована на комбінаторах, які були введені Шейнфінкелем у 1920 році разом з ідеєю створення аналогічного способу для побудови функцій та видалення будь-яких згадок про змінні, особливо в логіці предикатів. Комбінатор — це функція вищого порядку, яка використовує тільки застосування функції та раніше визначені комбінатори, щоб визначити результат на своїх аргументах. (uk) |
| dbo:wikiPageExternalLink | http://dkeenan.com/Lambda/index.htm http://www.angelfire.com/tx4/cus/combinator/birds.html https://web.archive.org/web/20081029051502/http:/cstein.kings.cam.ac.uk/~chris/combinators.html http://www.cip.ifi.lmu.de/~langeh/test/1924%20-%20Schoenfinkel%20-%20Ueber%20die%20Bausteine%20der%20mathematischen%20Logik.pdf https://www.wolfram-media.com/products/combinators-a-centennial-view.html http://code.google.com/p/clache http://www.cambridge.org/catalogue/catalogue.asp%3Fisbn=9780521898850 https://archive.org/details/CLP-2003_780 https://archive.org/details/functionalprogra0000fiel https://web.archive.org/web/20051016213140/http:/folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf https://web.archive.org/web/20070209093802/http:/www.sadl.uleth.ca/gsdl/cgi-bin/library%3Fa=p&p=about&c=curry https://web.archive.org/web/20160304083208/http:/tromp.github.io/cl/LC.pdf http://projecteuclid.org/euclid.jsl/1183743187%7Cmr=1043546%7Cjournal= http://plato.stanford.edu/entries/logic-combinatory/ http://www.cl.cam.ac.uk/Teaching/Lectures/founds-fp/Founds-FP.ps.gz | |
| dbo:wikiPageID | 149848 (xsd:integer) | |
| dbo:wikiPageLength | 42316 (xsd:nonNegativeInteger) | |
| dbo:wikiPageRevisionID | 1115981784 (xsd:integer) | |
| dbo:wikiPageWikiLink | dbr:Cambridge_University_Press dbr:B,_C,_K,_W_System dbr:Predicate_logic dbr:Princeton_University dbr:Q.E.D. dbr:Model_theory dbr:Non-strict_programming_language dbr:Belgium dbr:David_Turner_(computer_scientist) dbc:Lambda_calculus dbr:Applicative_computing_systems dbc:Combinatory_logic dbr:Beta_normal_form dbr:Cylindric_algebra dbr:University_of_Copenhagen dbr:University_of_Warsaw dbr:Unlambda dbr:Deduction_theorem dbr:Intuitionistic_logic dbr:Combinational_logic dbr:Combinatory_logic dbr:Computability_theory dbr:Mathematical_logic dbr:Normal_form_(abstract_rewriting) dbr:Free_variables_and_bound_variables dbr:Moses_Schönfinkel dbr:Stanford_Encyclopedia_of_Philosophy dbr:Combinatory_categorial_grammar dbr:Computation dbr:Computer_science dbr:Function_application dbr:Functional_programming dbr:Henk_Barendregt dbr:Kripke_semantics dbr:To_Mock_a_Mockingbird dbr:Willard_Van_Orman_Quine dbr:Katalin_Bimbó dbr:J_programming_language dbr:APL_(programming_language) dbr:Alonzo_Church dbr:Dana_Scott dbr:First-order_logic dbr:Formal_parameter dbr:Oxford_University_Press dbr:Church-Turing_thesis dbr:Church_encoding dbr:Graph_reduction_machine dbr:Journal_of_Symbolic_Logic dbr:Fixed_point_combinator dbr:Free_variable dbr:Predicate_functor_logic dbr:Robert_Feys dbr:Proof_theory dbr:Quantifier_(logic) dbr:Recursion dbr:Harvard_University_Press dbr:Haskell_Curry dbr:Higher-order_function dbr:Iota_and_Jot dbr:Jean_van_Heijenoort dbc:Logic_in_computer_science dbr:Kenneth_E._Iverson dbr:Lambda_calculus dbr:Big_O_notation dbr:B,_C,_K,_W_system dbr:Inclusion_(set_theory) dbr:Associative dbr:Categorical_abstract_machine dbr:Raymond_Smullyan dbr:Model_of_computation dbr:Turing_machine dbr:SKI_combinator_calculus dbr:Up_to dbr:Explicit_substitution dbr:Expressive_power_(computer_science) dbr:Tacit_programming dbr:SASL_programming_language dbr:Rice's_theorem dbr:Supercombinator dbr:Wolfram_Media dbr:North-Holland_Publishing_Company dbr:Functional_programming_languages dbr:Curry–Howard_isomorphism dbr:Extensional_equality dbr:Hilbert-style_deduction_system | |
| dbp:wikiPageUsesTemplate | dbt:Authority_control dbt:Citation dbt:Cite_book dbt:Cite_journal dbt:Distinguish dbt:ISBN dbt:Main dbt:Math dbt:Mvar dbt:Reflist dbt:Sfn dbt:Short_description dbt:Spaces dbt:Tmath dbt:!( dbt:Math_proof dbt:))! dbt:Mset | |
| dct:subject | dbc:Lambda_calculus dbc:Combinatory_logic dbc:Logic_in_computer_science | |
| gold:hypernym | dbr:Notation | |
| rdf:type | owl:Thing dbo:Software | |
| rdfs:comment | Kombinatorische Logik (Abgekürzt CL für engl. Combinatory Logic) ist eine Notation, die von Moses Schönfinkel und Haskell Brooks Curry eingeführt wurde, um die Verwendung von Variablen in der Mathematischen Logik zu vermeiden. Sie wird besonders in der Informatik als theoretisches Modell für Berechnung, als auch als Grundlage zum Design funktionaler Programmiersprachen eingesetzt. (de) Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments. (en) La lógica combinatoria es la lógica última y como tal puede ser un modelo simplificado del cómputo, usado en la teoría de la computabilidad (el estudio de qué puede ser computado) y la teoría de la prueba (el estudio de qué se puede probar matemáticamente). (es) コンビネータ論理（英: combinatory logic、組み合わせ論理）は、（露: Моисей Эльевич Шейнфинкель、英: Moses Ilyich Schönfinkel）とハスケル・カリー（英: Haskell Brooks Curry）によって、記号論理での変数を消去するために導入された記法である。最近では、計算機科学において計算の理論的モデルで利用されてきている。また、関数型プログラミング言語の理論（意味論など）や実装にも応用がある。 コンビネータ論理は、コンビネータまたは引数のみからなる関数適用によって結果が定義されている高階関数、コンビネータに基づいている。 (ja) De combinatorische logica (ook: combinatoire logica) was oorspronkelijk een door en Haskell Curry bedachte notatie in de wiskundige logica, waarmee de noodzakelijkheid van het gebruik van variabelen verdween. De laatste tijd wordt deze notatie vooral gebruikt in de computerwetenschap, meer in het bijzonder in de theoretische informatica en voor het ontwerpen van functionele programmeertalen. De notatie is gebaseerd op combinatoren in de vorm van een hogere-ordefunctie zonder vrije variabelen. (nl) Lógica combinatória é uma notação introduzida por Moses Schönfinkel e Haskell Curry para eliminar a necessidade de variáveis em lógica matemática. Vem sendo mais usada recentemente na ciência da computação como um modelo de computação e como base para o desenvolvimento de linguagens de programação funcionais. Ela é baseada em combinadores, somente usam aplicações de funções e outros combinadores para definir um resultado a partir de seus parâmetros. (pt) 组合子逻辑是和哈斯凱爾·加里介入的一种符号系统，用来消除数理逻辑中对变量的需要。它最近在计算机科学中被用做计算的理论模型和设计函数式编程语言的基础。它所基于的组合子是只使用函数应用或早先定义的组合子来定义从它们的参数得出的结果的高阶函数。 (zh) Комбінаторна логіка — це нотація для усунення необхідності кількісних змінних в математичній логіці. Вона була введена Мойсейем Шейнфінкелем і Гаскеллем Каррі, та використовується в інформатиці як теоретична модель обчислень, а також як основа для розробки функціональних мов програмування. Вона заснована на комбінаторах, які були введені Шейнфінкелем у 1920 році разом з ідеєю створення аналогічного способу для побудови функцій та видалення будь-яких згадок про змінні, особливо в логіці предикатів. Комбінатор — це функція вищого порядку, яка використовує тільки застосування функції та раніше визначені комбінатори, щоб визначити результат на своїх аргументах. (uk) La lògica combinatòria és la lògica última i com a tal pot ser un model simplificat del còmput, usat en la teoria de computabilitat (l'estudi de què pot ser computat) i la teoria de la prova (l'estudi de què es pot provar matemàticament). La teoria, a causa de la seva simplicitat, captura les característiques essencials de la naturalesa del còmput. La lògica combinatòria (LC) és el fonament del càlcul lambda, en eliminar el darrer tipus de variable d'aquest: la variable lambda. En LC les expressions lambda (usades per permetre l'abstracció funcional), són substituïdes per un sistema limitat de combinacions, les funcions primitives que no contenen cap ( ni lligada). És fàcil transformar expressions lambda en expressions combinatòries, i ja que la reducció d'un combinat és més simple que la (ca) En logique mathématique, la logique combinatoire est une théorie logique introduite par Moses Schönfinkel en 1920 lors d'une conférence et développée dès 1929 par Haskell Brooks Curry pour supprimer le besoin de variables en mathématiques, pour formaliser rigoureusement la notion de fonction et pour minimiser le nombre d'opérateurs nécessaires pour définir le calcul des prédicats à la suite de Henry M. Sheffer. Plus récemment, elle a été utilisée en informatique comme modèle théorique de calcul et comme base pour la conception de langages de programmation fonctionnels. (fr) Rachunek kombinatorów (ang. Combinatory Calculi) to jeden z najprostszych możliwych uniwersalnych systemów formalnych. Na język rachunku kombinatorów składają się kombinator stały K, kombinator rozdzielonej aplikacji S, oraz kombinatory aplikacji złożone z pary dowolnych kombinatorów - funkcji i argumentu: * σ = S | K | (σ σ) Derywacją rządzą dwie reguły: * ((K α) β) → α * (((S α) β) γ) → ((α γ) (β γ)) Gdzie α, β i γ to dowolne kombinatory. Tak prosty system jest w stanie wyrazić wszystko, co jest w stanie wyrazić rachunek lambda, dowolna maszyna Turinga czy w ogóle dowolny algorytm. * (I α) → α (pl) Комбина́торная ло́гика — направление математической логики, занимающееся фундаментальными (то есть не нуждающимися в объяснении и не анализируемыми) понятиями и методами формальных логических систем или исчислений. В дискретной математике комбинаторная логика тесно связана с лямбда-исчислением, так как описывает вычислительные процессы. (ru) |
| rdfs:label | Combinatory logic (en) Lògica combinatòria (ca) Kombinatorische Logik (de) Lógica combinatoria (es) Logique combinatoire (fr) コンビネータ論理 (ja) Combinatorische logica (nl) Rachunek kombinatorów (pl) Lógica combinatória (pt) Комбинаторная логика (ru) Комбінаторна логіка (uk) 组合子逻辑 (zh) | |
| owl:sameAs | freebase:Combinatory logic http://d-nb.info/gnd/4164750-6 wikidata:Combinatory logic dbpedia-az:Combinatory logic dbpedia-ca:Combinatory logic dbpedia-de:Combinatory logic dbpedia-es:Combinatory logic dbpedia-fr:Combinatory logic dbpedia-gd:Combinatory logic dbpedia-gl:Combinatory logic dbpedia-hr:Combinatory logic http://hy.dbpedia.org/resource/Կոմբինատորային_տրամաբանություն dbpedia-ja:Combinatory logic dbpedia-nl:Combinatory logic dbpedia-no:Combinatory logic dbpedia-pl:Combinatory logic dbpedia-pt:Combinatory logic dbpedia-ru:Combinatory logic dbpedia-sh:Combinatory logic dbpedia-uk:Combinatory logic dbpedia-zh:Combinatory logic https://global.dbpedia.org/id/UGF5 | |
| prov:wasDerivedFrom | wikipedia-en:Combinatory_logic?oldid=1115981784&ns=0 | |
| foaf:isPrimaryTopicOf | wikipedia-en:Combinatory_logic | |
| is dbo:knownFor of | dbr:Moses_Schönfinkel dbr:Haskell_Curry | |
| is dbo:wikiPageRedirects of | dbr:K_combinator dbr:Abstraction_elimination dbr:S_combinator dbr:Combinatory_Logic dbr:S-combinator dbr:Lambda_elimination dbr:Combinator dbr:Combinator_calculus dbr:Combinatorial_logic_(mathematics) dbr:Combinators dbr:Combinatory_algebra | |
| is dbo:wikiPageWikiLink of | dbr:Probabilistic_logic_network dbr:Propositional_calculus dbr:List_of_computability_and_complexity_topics dbr:Normalisation_by_evaluation dbr:Dependent_type dbr:Anonymous_recursion dbr:Applicative_computing_systems dbr:Applicative_universal_grammar dbr:History_of_the_function_concept dbr:Richard_Statman dbr:Curry's_paradox dbr:Cylindric_algebra dbr:Unlambda dbr:De_Bruijn_index dbr:Deduction_theorem dbr:Deductive_lambda_calculus dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(A–C) dbr:List_of_mathematical_logic_topics dbr:List_of_mathematical_proofs dbr:K_combinator dbr:Substructural_type_system dbr:Combinational_logic dbr:Combinatory_logic dbr:Computability dbr:Corrado_Böhm dbr:Mathematical_logic dbr:Omega dbr:Scott–Curry_theorem dbr:Church–Turing_thesis dbr:Free_variables_and_bound_variables dbr:Function_composition dbr:Moses_Schönfinkel dbr:Constructive_set_theory dbr:Simply_typed_lambda_calculus dbr:Combinator_library dbr:Combinatory_categorial_grammar dbr:Computable_topology dbr:Functional_programming dbr:Program_counter dbr:Mark_Steedman dbr:Theory_of_computation dbr:To_Mock_a_Mockingbird dbr:Type_theory dbr:Lambda_calculus_definition dbr:Laws_of_Form dbr:Lazy_evaluation dbr:Algebraic_logic dbr:Curry–Howard_correspondence dbr:Eugene_McDonnell dbr:Fixed_point_(mathematics) dbr:Abstraction_elimination dbr:Parameter dbr:List_of_Russian_mathematicians dbr:List_of_Russian_scientists dbr:Predicate_functor_logic dbr:Haskell_Curry dbr:Higher-order_function dbr:Hilbert_system dbr:Hindley–Milner_type_system dbr:Iota_and_Jot dbr:Abstract_algebraic_logic dbr:Lambda_calculus dbr:Binary_combinatory_logic dbr:B,_C,_K,_W_system dbr:Greek_letters_used_in_mathematics,_science,_and_engineering dbr:Categorial_grammar dbr:Categorical_abstract_machine dbr:Raymond_Smullyan dbr:Word_problem_(mathematics) dbr:Kleene–Rosser_paradox dbr:Model_of_computation dbr:S_combinator dbr:SKI_combinator_calculus dbr:Explicit_substitution dbr:Combinatory_Logic dbr:Fixed-point_combinator dbr:Tacit_programming dbr:List_of_Russian_people dbr:Outline_of_software_engineering dbr:S-combinator dbr:Lambda_elimination dbr:Combinator dbr:Combinator_calculus dbr:Combinatorial_logic_(mathematics) dbr:Combinators dbr:Combinatory_algebra | |
| is dbp:knownFor of | dbr:Moses_Schönfinkel dbr:Haskell_Curry | |
| is foaf:primaryTopic of | wikipedia-en:Combinatory_logic |