| dbpedia-owl:abstract
|
- System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by the logician Jean-Yves Girard and the computer scientist John C. Reynolds. Whereas simply typed lambda calculus has variables ranging over functions, and binders for them, System F additionally has variables ranging over types, and binders for them. As an example, the fact that the identity function can have any type of the form A→ A would be formalized in System F as the judgment where α is a type variable. The upper-case is traditionally used to denote type-level functions, as opposed to the lower-case which is used for value-level functions. As a term rewriting system, System F is strongly normalizing. Type inference in System F (without explicit type annotations) is undecidable however. Under the Curry–Howard isomorphism, System F corresponds to the fragment of second-order intuitionistic logic that uses only universal quantification. System F can be seen as part of the lambda cube, together with even more expressive typed lambda calculi, including those with dependent types.
- Il Sistema F, anche conosciuto come lambda calcolo polimorfico o lambda calcolo di secondo ordine, è un lambda calcolo tipato. È stato scoperto indipendentemente da logico Jean-Yves Girard e dall'informatico John C. Reynolds. Il Sistema F formalizza la nozione di polimorfismo parametrico nei linguaggi di programmazione e pone le basi per linguaggi come Haskell, ML, e F#. Come sistema di riscrittura di termini, è fortemente normalizzante. Come il lambda calcolo è composto da variabili sulle funzioni e relativi binder, così il lambda calcolo di secondo ordine ha variabili sui tipi e relativi binder. Ad esempio, il fatto che la funzione identità può essere di qualunque tipo della forma A→ A può essere formalizzato nel sistema F come segue: dove α è una variabile di tipo. Il maiuscolo è usato tradizionalmente per indicare funzioni a livello di tipi, mentre il minuscolo viene usato per le funzioni a livello di valori. Sotto l'isomorfismo di Curry-Howard, il Sistema F corrisponde a una logica proposizionale di secondo ordine. Il Sistema F può essere visto come parte del lambda cubo, insieme ad altri lambda calcoli tipati più espressivi, inclusi quelli con solo tipi dipendenti.
- System F – jeden z wariantów rachunku lambda z typami. Jest to najprostszy rachunek zawierający typy proste oraz typy polimorficzne. Zbiór typów można zdefiniować jako najmniejszy taki zbiór U, że przy danym, ustalonym i przeliczalnym zbiorze zmiennych V, zachodzą następujące własności: V zawiera się w U, jeśli oraz należą do U, to również należy do U, jeśli jest zmienną (należy do V) oraz należy do U, to również należy do U. Typy postaci należy traktować (nieformalnie) jako każdą możliwą instancję typu taką, że za każde wystąpienie zmiennej wstawiamy dowolny inny typ (za każde wystąpienie zmiennej ten sam).
- 系统F，也叫做多态 lambda 演算或二阶 lambda 演算，是有类型 lambda 演算。它由逻辑学家 Jean-Yves Girard 和计算机科学家 John C. Reynolds 独立发现的。系统F 形式化了编程语言中的参数多态的概念。 正如同 lambda 演算有取值于（rang over）函数的变量，和来自它们的粘合子（binder）；二阶 lambda 演算取值自类型，和来自它们的粘合子。 作为一个例子，恒等函数有形如 A→ A 的任何类型的事实可以在系统F 中被形式化为判断 这里的 α 是类型变量。 在 Curry-Howard同构下，系统F 对应于二阶逻辑。 系统F，和甚至更加有表达力的 lambda 演算一起，可被看作 Lambda立方体的一部分。
- Le système F (également connu sous le nom de lambda-calcul polymorphe ou de lambda-calcul du second ordre) est une extension du lambda-calcul simplement typé introduite indépendamment par le logicien Jean-Yves Girard et par l'informaticien John C. Reynolds. Ce système se distingue du lambda-calcul simplement typé par l'introduction d'un mécanisme de quantification universelle de type qui permet d'exprimer le polymorphisme paramétrique. Ainsi que l'atteste sa double origine, le système F peut être étudié dans deux contextes très différents: Dans le domaine de la programmation fonctionnelle, où il apparaît comme une extension très expressive du noyau du langage ML. Son expressivité est illustrée par le fait que les types de données courants (booléens, entiers, listes, etc. ) sont définissables dans le système F à partir des constructions de base. Dans le domaine de la logique, et plus particulièrement de la théorie de la démonstration. À travers la correspondance de Curry-Howard, le système F est en effet isomorphe à la logique minimale intuitionniste du second ordre. En outre, ce système capture très exactement la classe des fonctions numériques dont l'existence est prouvable en arithmétique intuitionniste du second ordre (parfois appelée analyse intuitionniste). C'est d'ailleurs cette propriété remarquable du système F qui a historiquement motivé son introduction par Jean-Yves Girard, dans la mesure où cette propriété permet de résoudre le problème de l'élimination des coupures en arithmétique du second ordre, conjecturé par Takeuti. Comme le lambda-calcul simplement typé, le système F admet deux présentations équivalentes: Une présentation à la Church, dans laquelle chaque terme contient toutes les annotations de type nécessaires à la reconstruction de son type (de manière univoque). Une présentation à la Curry, due à l'informaticien Daniel Leivant, dans laquelle les termes (qui sont ceux du lambda-calcul pur) sont dépourvus de toute annotation de type, et sont ainsi sujets aux problèmes d'ambiguïté typique.
|
| rdfs:comment
|
- 系统F，也叫做多态 lambda 演算或二阶 lambda 演算，是有类型 lambda 演算。它由逻辑学家 Jean-Yves Girard 和计算机科学家 John C. Reynolds 独立发现的。系统F 形式化了编程语言中的参数多态的概念。 正如同 lambda 演算有取值于（rang over）函数的变量，和来自它们的粘合子（binder）；二阶 lambda 演算取值自类型，和来自它们的粘合子。 作为一个例子，恒等函数有形如 A→ A 的任何类型的事实可以在系统F 中被形式化为判断 这里的 α 是类型变量。 在 Curry-Howard同构下，系统F 对应于二阶逻辑。 系统F，和甚至更加有表达力的 lambda 演算一起，可被看作 Lambda立方体的一部分。
- System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML.
- Il Sistema F, anche conosciuto come lambda calcolo polimorfico o lambda calcolo di secondo ordine, è un lambda calcolo tipato. È stato scoperto indipendentemente da logico Jean-Yves Girard e dall'informatico John C. Reynolds. Il Sistema F formalizza la nozione di polimorfismo parametrico nei linguaggi di programmazione e pone le basi per linguaggi come Haskell, ML, e F#. Come sistema di riscrittura di termini, è fortemente normalizzante.
- System F – jeden z wariantów rachunku lambda z typami. Jest to najprostszy rachunek zawierający typy proste oraz typy polimorficzne. Zbiór typów można zdefiniować jako najmniejszy taki zbiór U, że przy danym, ustalonym i przeliczalnym zbiorze zmiennych V, zachodzą następujące własności: V zawiera się w U, jeśli oraz należą do U, to również należy do U, jeśli jest zmienną (należy do V) oraz należy do U, to również należy do U.
- Le système F (également connu sous le nom de lambda-calcul polymorphe ou de lambda-calcul du second ordre) est une extension du lambda-calcul simplement typé introduite indépendamment par le logicien Jean-Yves Girard et par l'informaticien John C. Reynolds. Ce système se distingue du lambda-calcul simplement typé par l'introduction d'un mécanisme de quantification universelle de type qui permet d'exprimer le polymorphisme paramétrique.
|
