This HTML5 document contains 121 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

Prefix	IRI
dcterms	http://purl.org/dc/terms/
dbo	http://dbpedia.org/ontology/
foaf	http://xmlns.com/foaf/0.1/
dbpedia-es	http://es.dbpedia.org/resource/
n21	https://global.dbpedia.org/id/
n10	http://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-381/
dbpedia-ru	http://ru.dbpedia.org/resource/
dbt	http://dbpedia.org/resource/Template:
rdfs	http://www.w3.org/2000/01/rdf-schema#
freebase	http://rdf.freebase.com/ns/
dbpedia-pt	http://pt.dbpedia.org/resource/
dbpedia-el	http://el.dbpedia.org/resource/
n19	ftp://ftp.cs.ru.nl/pub/CompMath.Found/
rdf	http://www.w3.org/1999/02/22-rdf-syntax-ns#
owl	http://www.w3.org/2002/07/owl#
dbpedia-zh	http://zh.dbpedia.org/resource/
wikipedia-en	http://en.wikipedia.org/wiki/
dbp	http://dbpedia.org/property/
dbc	http://dbpedia.org/resource/Category:
prov	http://www.w3.org/ns/prov#
xsdh	http://www.w3.org/2001/XMLSchema#
wikidata	http://www.wikidata.org/entity/
dbr	http://dbpedia.org/resource/

Statements

Subject Item

dbr:Simply_typed_lambda_calculus

rdfs:label

Cálculo lambda simplesmente tipado Cálculo lambda simplemente tipado Λ-λογισμός με απλούς τύπους Просто типизированное лямбда-исчисление 简单类型λ演算 Simply typed lambda calculus

rdfs:comment

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. Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система ) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году. 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. 简单类型 lambda 演算是连接词只有 (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、或自然数(系统 T)甚至完全的递归(如)。相反的，介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。 Ο λ-λογισμός με απλούς τύπους είναι μια θεωρίας τύπων, είναι μια ερμηνεία τύπων του λ-λογισμού με ένα μοναδικό κατασκευαστή τύπων (type constructor): , ο οποίος κατασκευάζει . Είναι το κανονικό και το πιο απλό παράδειγμα λ-λογισμού με τύπους, και εμφανίζει πολλές επιθυμητές και ενδιαφέρουσες ιδιότητες. 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.

dcterms:subject

dbc:Theory_of_computation dbc:Lambda_calculus dbc:Type_theory

dbo:wikiPageID

1986011

dbo:wikiPageRevisionID

1122932982

dbo:wikiPageWikiLink

dbr:Operational_semantics dbr:Programming_language_for_Computable_Functions dbr:Joachim_Lambek dbr:Function_space dbr:Evaluation_strategy dbr:Type_erasure dbr:Function_type dbr:Coproduct dbr:Combinatory_logic dbr:Minimal_logic dbr:Closed_monoidal_category dbr:LF_(logical_framework) dbr:Typed_lambda_calculus dbr:Cartesian_closed_categories dbr:Internal_language dbr:Simply_typed_lambda_calculus dbr:Hindley–Milner_type_inference dbr:Dependent_type dbc:Theory_of_computation dbr:Product_(category_theory) dbr:Strong_normalization dbr:Object_(category_theory) dbr:Recursive_type dbr:Polynomial dbr:Final_object dbr:Intuitionistic_logic dbr:Set_(mathematics) dbr:Completeness_(logic) dbr:Turing_complete dbr:Lambda_calculus dbr:Backus–Naur_form dbr:Equivalence_class dbr:Unification_(computing) dbr:Apply dbr:Currying dbr:Dialectica_interpretation dbr:Type_inhabitation dbc:Lambda_calculus dbr:Set_theory dbr:Untyped_lambda_calculus dbr:Elementary_recursive dbr:Morphism dbr:Cartesian_product dbr:Decidability_(logic) dbr:Type_constructor dbr:Parametric_polymorphism dbr:Grzegorczyk_hierarchy dbr:Recursion dbr:Alonzo_Church dbr:Type_system dbr:Call_by_value dbr:Type_theory dbr:Call_by_name dbr:Type_inference dbr:Typing_environment dbr:System_F dbr:Equational_theory dbr:Church_encoding dbr:Typing_rule dbr:Eta_reduction dbc:Type_theory dbr:Tautology_(logic) dbr:Church_numeral dbr:Curry–Howard_isomorphism dbr:Beta_reduction dbr:Principal_type dbr:Fixed-point_combinator dbr:Normalisation_by_evaluation dbr:Functor dbr:Type_safety dbr:Linear_type_system dbr:Category_of_sets dbr:Natural_number dbr:Topos dbr:Natural_deduction dbr:Normalization_property_(lambda-calculus)

dbo:wikiPageExternalLink

n10: n19:HBK.ps

owl:sameAs

dbpedia-el:Λ-λογισμός_με_απλούς_τύπους freebase:m.06c09x dbpedia-pt:Cálculo_lambda_simplesmente_tipado wikidata:Q855192 dbpedia-ru:Просто_типизированное_лямбда-исчисление dbpedia-zh:简单类型λ演算 n21:51GJQ dbpedia-es:Cálculo_lambda_simplemente_tipado

dbp:wikiPageUsesTemplate

dbt:Mono dbt:Short_description dbt:Cite_web dbt:Cite_journal dbt:Reflist dbt:SEP dbt:R dbt:Isbn dbt:Tone

dbo:abstract

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. Просто типизированное лямбда-исчисление (простое типизированное лямбда-исчисление, лямбда-исчисление с простыми типами, система ) — система типизированного лямбда-исчисления, в которой лямбда-абстракции приписывается специальный «стрелочный» тип. Эта система была предложена Алонзо Чёрчем в 1940 году. Для близкого к лямбда-исчислению формализма комбинаторной логики похожая система рассматривалась Хаскеллом Карри в 1934 году. 简单类型 lambda 演算是连接词只有 (函数类型)的有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。 简单类型也被用来称呼对简单类型 lambda 演算的扩展比如积、或自然数(系统 T)甚至完全的递归(如)。相反的，介入了多态类型(如系统F)或依赖类型(如逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由阿隆佐·邱奇在 1940 年介入来尝试避免无类型 lambda 演算的悖论性使用。 Ο λ-λογισμός με απλούς τύπους είναι μια θεωρίας τύπων, είναι μια ερμηνεία τύπων του λ-λογισμού με ένα μοναδικό κατασκευαστή τύπων (type constructor): , ο οποίος κατασκευάζει . Είναι το κανονικό και το πιο απλό παράδειγμα λ-λογισμού με τύπους, και εμφανίζει πολλές επιθυμητές και ενδιαφέρουσες ιδιότητες. Ο όρος απλός τύπος χρησιμοποιείται επίσης για επεκτάσεις του λ-λογισμού με απλούς τύπους όπως τα γινόμενα, τα συγγινόμενα, και οι φυσικοί αριθμοί ή ακόμη και με πλήρη αναδρομή. Αντίθετα, συστήματα που εισάγουν (όπως το Σύστημα F) ή εξαρτώμενους τύπους όπως το δεν θεωρούνται με απλούς τύπους. Τα πρώτα θεωρούνται απλά επειδή μπορεί να γίνει κωδικοποίηση Τσερτς τέτοιων δομών χρησιμοποιώντας μόνο και κατάλληλες μεταβλητές τύπων, ενώ δεν μπορούν να κωδικοποιηθούν αντίστοιχα ο πολυμορφισμός και η εξάρτηση τύπων. 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. 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.

prov:wasDerivedFrom

wikipedia-en:Simply_typed_lambda_calculus?oldid=1122932982&ns=0

dbo:wikiPageLength

29326

foaf:isPrimaryTopicOf

wikipedia-en:Simply_typed_lambda_calculus