| 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)
|
| 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)
|
