Simply typed lambda calculus (original) (raw)
Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система ) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году.
Property | Value |
---|---|
dbo:abstract | Ο λ-λογισμός με απλούς τύπους είναι μια θεωρίας τύπων, είναι μια ερμηνεία τύπων του λ-λογισμού με ένα μοναδικό κατασκευαστή τύπων (type constructor): , ο οποίος κατασκευάζει . Είναι το κανονικό και το πιο απλό παράδειγμα λ-λογισμού με τύπους, και εμφανίζει πολλές επιθυμητές και ενδιαφέρουσες ιδιότητες. Ο όρος απλός τύπος χρησιμοποιείται επίσης για επεκτάσεις του λ-λογισμού με απλούς τύπους όπως τα γινόμενα, τα συγγινόμενα, και οι φυσικοί αριθμοί ή ακόμη και με πλήρη αναδρομή. Αντίθετα, συστήματα που εισάγουν (όπως το Σύστημα F) ή εξαρτώμενους τύπους όπως το δεν θεωρούνται με απλούς τύπους. Τα πρώτα θεωρούνται απλά επειδή μπορεί να γίνει κωδικοποίηση Τσερτς τέτοιων δομών χρησιμοποιώντας μόνο και κατάλληλες μεταβλητές τύπων, ενώ δεν μπορούν να κωδικοποιηθούν αντίστοιχα ο πολυμορφισμός και η εξάρτηση τύπων. (el) El cálculo lambda simplemente tipado es una teoría de tipos basada en el cálculo de lambda con un único , , que construye . Es el ejemplo canónico y más sencillo de un cálculo lambda tipado. El cálculo lambda simplemente tipado fue originalmente introducido por Alonzo Church en el 1940 como un intento de evitar la aparición de paradojas en el cálculo lambda sin tipos. El término simplemente tipado es también utilizado para referirse a extensiones del cálculo lambda simplemente tipado con productos, coproductos, números naturales o incluso recursión (como en el lenguaje PCF). En contraste, los sistemas que introducen tipos polimórficos (como ) o (como el ) no se consideran simplemente tipados. Los primeros, excepto aquellos que implementan recursión arbitraria, se consideran todavía simplemente tipados porque la de estas estructuras puede hacerse utilizando solamente y variables de tipo, mientras que el polimorfismo y la dependencia no pueden expresarse de esta forma. (es) The simply typed lambda calculus, a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus. The term simple type is also used to refer extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF). In contrast, systems which introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered simply typed. The simple types, except for full recursion, are still considered simple because the Church encodings of such structures can be done using only and suitable type variables, while polymorphism and dependency cannot. (en) O cálculo lambda simplesmente tipado, ou cálculo lambda com tipagem simples, é um modelo da teoria dos tipos que adiciona o conceito de tipagem ao cálculo lambda. Isso é possível com adição de apenas um elemento (o construtor de tipos: ) para construir tipos de funções. Esse é o exemplo mais simples e canônico de um cálculo lambda com tipagem. O cálculo lambda simplesmente tipado foi introduzido originalmente por Alonzo Church em 1940 como uma tentativa de evitar o uso paradoxal do , o qual mostrou várias propriedades interessantes e desejadas. O termo tipo simples também é utilizado para se referir à extensões do cálculo lambda simplesmente tipado como produtos, coprodutos, números naturais ou até recursão completa. Em contraste, sistemas que introduzem tipos polimórficos (como o ) ou não são considerados simplesmente tipados. O cálculo lambda simplesmente tipado é considerado simples por conta da Codificação de Church de suas estruturas que pode ser feita usando apenas o símbolo e variáveis de tipos adequadas, enquanto polimorfismo e dependência não podem. (pt) Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система ) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году. (ru) 简单类型 lambda 演算是连接词只有 (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、或自然数(系统 T)甚至完全的递归(如)。相反的,介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。 (zh) |
dbo:wikiPageExternalLink | ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps http://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-381/ |
dbo:wikiPageID | 1986011 (xsd:integer) |
dbo:wikiPageLength | 29326 (xsd:nonNegativeInteger) |
dbo:wikiPageRevisionID | 1122932982 (xsd:integer) |
dbo:wikiPageWikiLink | dbr:Cartesian_product dbr:Normalisation_by_evaluation dbr:Typed_lambda_calculus dbr:Principal_type dbr:Beta_reduction dbr:Dependent_type dbc:Lambda_calculus dbr:Apply dbr:Currying dbr:Call_by_name dbr:Call_by_value dbr:Decidability_(logic) dbr:Intuitionistic_logic dbr:Combinatory_logic dbr:Morphism dbr:Coproduct dbr:Equivalence_class dbr:Operational_semantics dbr:Linear_type_system dbr:Simply_typed_lambda_calculus dbr:Closed_monoidal_category dbr:Completeness_(logic) dbr:Function_space dbr:Function_type dbr:Functor dbr:Parametric_polymorphism dbr:Turing_complete dbr:Typing_environment dbr:Backus–Naur_form dbr:Category_of_sets dbr:Type_system dbr:Type_theory dbr:Eta_reduction dbr:Minimal_logic dbr:Alonzo_Church dbr:Church_encoding dbr:Dialectica_interpretation dbr:Natural_deduction dbr:Type_erasure dbr:Product_(category_theory) dbr:Recursion dbr:Tautology_(logic) dbc:Theory_of_computation dbc:Type_theory dbr:Joachim_Lambek dbr:LF_(logical_framework) dbr:Lambda_calculus dbr:Topos dbr:System_F dbr:Polynomial dbr:Grzegorczyk_hierarchy dbr:Typing_rule dbr:Natural_number dbr:Set_(mathematics) dbr:Set_theory dbr:Type_safety dbr:Type_inference dbr:Untyped_lambda_calculus dbr:Type_inhabitation dbr:Evaluation_strategy dbr:Fixed-point_combinator dbr:Internal_language dbr:Type_constructor dbr:Normalization_property_(lambda-calculus) dbr:Elementary_recursive dbr:Church_numeral dbr:Equational_theory dbr:Strong_normalization dbr:Cartesian_closed_categories dbr:Final_object dbr:Programming_language_for_Computable_Functions dbr:Recursive_type dbr:Object_(category_theory) dbr:Unification_(computing) dbr:Curry–Howard_isomorphism dbr:Hindley–Milner_type_inference |
dbp:wikiPageUsesTemplate | dbt:Cite_journal dbt:Cite_web dbt:Mono dbt:R dbt:Reflist dbt:Short_description dbt:Tone dbt:Isbn dbt:SEP |
dcterms:subject | dbc:Lambda_calculus dbc:Theory_of_computation dbc:Type_theory |
rdfs:comment | Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система ) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году. (ru) 简单类型 lambda 演算是连接词只有 (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、或自然数(系统 T)甚至完全的递归(如)。相反的,介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。 (zh) Ο λ-λογισμός με απλούς τύπους είναι μια θεωρίας τύπων, είναι μια ερμηνεία τύπων του λ-λογισμού με ένα μοναδικό κατασκευαστή τύπων (type constructor): , ο οποίος κατασκευάζει . Είναι το κανονικό και το πιο απλό παράδειγμα λ-λογισμού με τύπους, και εμφανίζει πολλές επιθυμητές και ενδιαφέρουσες ιδιότητες. (el) El cálculo lambda simplemente tipado es una teoría de tipos basada en el cálculo de lambda con un único , , que construye . Es el ejemplo canónico y más sencillo de un cálculo lambda tipado. El cálculo lambda simplemente tipado fue originalmente introducido por Alonzo Church en el 1940 como un intento de evitar la aparición de paradojas en el cálculo lambda sin tipos. (es) The simply typed lambda calculus, a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus. (en) O cálculo lambda simplesmente tipado, ou cálculo lambda com tipagem simples, é um modelo da teoria dos tipos que adiciona o conceito de tipagem ao cálculo lambda. Isso é possível com adição de apenas um elemento (o construtor de tipos: ) para construir tipos de funções. Esse é o exemplo mais simples e canônico de um cálculo lambda com tipagem. O cálculo lambda simplesmente tipado foi introduzido originalmente por Alonzo Church em 1940 como uma tentativa de evitar o uso paradoxal do , o qual mostrou várias propriedades interessantes e desejadas. (pt) |
rdfs:label | Λ-λογισμός με απλούς τύπους (el) Cálculo lambda simplemente tipado (es) Simply typed lambda calculus (en) Cálculo lambda simplesmente tipado (pt) Просто типизированное лямбда-исчисление (ru) 简单类型λ演算 (zh) |
owl:sameAs | freebase:Simply typed lambda calculus wikidata:Simply typed lambda calculus dbpedia-el:Simply typed lambda calculus dbpedia-es:Simply typed lambda calculus dbpedia-pt:Simply typed lambda calculus dbpedia-ru:Simply typed lambda calculus dbpedia-zh:Simply typed lambda calculus https://global.dbpedia.org/id/51GJQ |
prov:wasDerivedFrom | wikipedia-en:Simply_typed_lambda_calculus?oldid=1122932982&ns=0 |
foaf:isPrimaryTopicOf | wikipedia-en:Simply_typed_lambda_calculus |
is dbo:knownFor of | dbr:Alonzo_Church |
is dbo:wikiPageDisambiguates of | dbr:STLC |
is dbo:wikiPageRedirects of | dbr:Bidirectional_type_checking dbr:Simply-typed_lambda_calculus dbr:Simply_typed_lambda dbr:Simply_typed_lambda-calculus dbr:Simply_typed_λ-calculus dbr:Simply_typed_λ_calculus dbr:Λ→ |
is dbo:wikiPageWikiLink of | dbr:Categorical_logic dbr:Q0_(mathematical_logic) dbr:Normalisation_by_evaluation dbr:Typed_lambda_calculus dbr:Dependent_type dbr:Apply dbr:Richard_Statman dbr:Curry's_paradox dbr:Currying dbr:Intersection_type_discipline dbr:List_of_mathematical_logic_topics dbr:Substructural_type_system dbr:Generalized_algebraic_data_type dbr:Nominal_terms_(computer_science) dbr:Normal_form_(abstract_rewriting) dbr:Simply_typed_lambda_calculus dbr:Bidirectional_type_checking dbr:Function_type dbr:Pure_type_system dbr:Markov's_principle dbr:Tuple dbr:Type_theory dbr:Lambda_cube dbr:Primitive_recursive_functional dbr:Minimal_logic dbr:Alonzo_Church dbr:Curry–Howard_correspondence dbr:POPLmark_challenge dbr:Church–Rosser_theorem dbr:History_of_type_theory dbr:Judgment_(mathematical_logic) dbr:Kind_(type_theory) dbr:Robert_Feys dbr:Gérard_Huet dbr:Hindley–Milner_type_system dbr:Joachim_Lambek dbr:Lambda_calculus dbr:Hom_functor dbr:System_F dbr:Greek_letters_used_in_mathematics,_science,_and_engineering dbr:Typing_rule dbr:Cartesian_closed_category dbr:Categorial_grammar dbr:Meta-circular_evaluator dbr:STLC dbr:Type_inference dbr:Type_inhabitation dbr:Subtyping dbr:Eval dbr:First-class_function dbr:Fixed-point_combinator dbr:Type_constructor dbr:Turing_completeness dbr:William_Alvin_Howard dbr:Simply-typed_lambda_calculus dbr:Simply_typed_lambda dbr:Simply_typed_lambda-calculus dbr:Simply_typed_λ-calculus dbr:Simply_typed_λ_calculus dbr:Λ→ |
is dbp:knownFor of | dbr:Alonzo_Church |
is foaf:primaryTopic of | wikipedia-en:Simply_typed_lambda_calculus |