| dbo:abstract
|
- To Σύστημα F, επίσης γνωστό ως πολυμορφικός λ-λογισμός των Ζιράρ-Ρέινολντς και λ-λογισμός δευτέρας τάξης, είναι ένας λ-λογισμός με τύπους που επεκτείνει τον λ-λογισμό με απλούς τύπους εισάγοντας ένα μηχανισμό καθολικής ποσόδειξης επί των τύπων. Ως εκ τούτου, το Σύστημα F αποτελεί φορμαλισμό της έννοιας του παραμετρικού πολυμορφισμού στις γλώσσες προγραμματισμού, και μια θεωρητική βάση γλωσσών όπως η Haskell και η ML. Το Σύστημα F επινοήθηκε ανεξάρτητα από τον και τον . Επεκτείνοντας το λ-λογισμό με απλούς τύπους που έχει μεταβλητές επί των όρων, το Σύστημα F έχει επιπρόσθετα μεταβλητές επί των τύπων. Για παράδειγμα, το γεγονός ότι η ταυτοτική συνάρτηση μπορεί να έχει οιονδήποτε τύπο της μορφής A→ A γράφεται στο Σύστημα F ως όπου α είναι . Το κεφαλαίο χρησιμοποιείται συνήθως για να εκφράσει συναρτήσεις στο επίπεδο των τύπων, σε αντιπαραβολή με το πεζό που χρησιμοποιείται για συναρτήσεις στο επίπεδο των όρων. Ως ένα , το Σύστημα F είναι ισχυρά κανονικοποιήσιμο. Η εξαγωγή τύπων στο Σύστημα F χωρίς ρητές επισημειώσεις τύπων είναι ωστόσο μη αποφάνσιμη. Με τον το Σύστημα F αντιστοιχίζεται στην δευτέρας τάξης με μόνη την καθολική ποσόδειξη. Το Σύστημα F μπορεί να θεωρηθεί τμήμα του , μαζί με εκφραστικότερους λ-λογισμούς με τύπους, συμπεριλαμβανομένων αυτών με εξαρτώμενους τύπους. (el)
- Le système F est un formalisme logique qui permet d'exprimer de façon très riche et très rigoureuse des fonctions et d'y démontrer formellement des propriétés difficiles. Plus précisément, 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'existence d'une quantification universelle sur les types qui permet d'exprimer du polymorphisme. Le système F possède deux propriétés cruciales : 1.
* la réduction des termes est fortement normalisante (dit plus crûment : tous les calculs se terminent) ; 2.
* il correspond par la correspondance de Curry-Howard à la logique minimale propositionnelle du second ordre. Soit : le calcul propositionnel, sans la négation mais avec les quantificateurs. Note liminaire : La lecture de cet article suppose la lecture préalable de l'article « lambda-calcul » et son assimilation . (fr)
- System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphism in programming languages, thus forming a theoretical basis for languages such as Haskell and ML. It was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974). Whereas simply typed lambda calculus has variables ranging over terms, 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. (The superscripted means that the bound x is of type ; the expression after the colon is the type of the lambda expression preceding it.) As a term rewriting system, System F is strongly normalizing. However, type inference in System F (without explicit type annotations) is undecidable. 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. According to Girard, the "F" in System F was picked by chance. (en)
- System F（システム・エフ）は、型付きラムダ計算の一体系であり、単純型付きラムダ計算に、型についての全称量化を取り入れた計算機構である。二階ラムダ計算、ポリモーフィックラムダ計算とも言われる。プログラミング言語でのを形式化するもので、関数型言語のMLやHaskellなどの型システムのベース理論にされている。System Fは、論理学者のジャン＝イヴ・ジラールと計算機科学者のの両者が別個に発見している。ジラールによるとSystem Fの語源は、たまたまそう名付けただけと言う。 単純型付きラムダ計算では、関数についての変数とその束縛が存在するが、System Fでは型についての変数とその束縛が追加されている。例えば恒等関数は任意の型についての形の型を持ちうるが、System Fではこのことが次の判断が成り立つことによって表されている。 . ここで、はである。また、小文字のが通常の値レベルの抽象を表しているのに対して、大文字のを型レベルの抽象を表すために使用している。 項書換え系として見ると、System Fはを持つ。しかしながらSystem Fにおける型推論は決定不能である。またSystem Fはカリー＝ハワード同型の下で、全称量化のみを用いる二階直観主義論理の断片に対応する。System Fは、依存型などを含んだより強力なラムダ計算とともに、ラムダ・キューブの一角であるとみなすこともできる。 (ja)
- Il sistema F, anche conosciuto come lambda calcolo polimorfico o lambda calcolo di secondo ordine, è un . È stato scoperto indipendentemente dal logico e dall'informatico . Il sistema F formalizza la nozione di polimorfismo parametrico nei linguaggi di programmazione e pone le basi per linguaggi come , ML, e . Come sistema di riscrittura di termini, è . (it)
- 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). (pl)
- Система F (полиморфное лямбда-исчисление, система , типизированное лямбда-исчисление второго порядка) — система типизированного лямбда-исчисления, отличающаяся от просто типизированной системы наличием механизма универсальной квантификации над типами. Эту систему разработал в 1972 году Жан-Ив Жирар в контексте теории доказательств в логике. Независимо от него подобную систему предложил в 1974 году Джон Рейнольдс. Система F позволяет формализовать концепцию параметрического полиморфизма в языках программирования и служит теоретической основой для таких языков программирования как Haskell и ML. Система F допускает конструирование термов, зависящих от типов. Технически это достигается через механизм абстрагирования терма по типу, что в результате даёт новый терм. Традиционно для такой абстракции используют символ большой лямбды . Например, взяв терм типа и абстрагируясь по переменной типа , получаем терм . Этот терм представляет собой функцию из типов в термы. Применяя эту функцию к различным типам, мы будем получать термы с идентичной структурой, но разными типами: — терм типа ; — терм типа . Видно, что терм обладает полиморфным поведением, то есть задаёт общий интерфейс для различных типов данных. В Системе F этому терму приписывается тип . Квантор всеобщности в типе подчёркивает возможность подстановки вместо переменной типа любого допустимого типа. (ru)
- 系统F，也叫做多态lambda演算或二阶lambda演算，是有类型lambda演算。它由逻辑学家和计算机科学家独立发现的。系统F形式化了编程语言中的参数多态的概念。 正如同lambda演算有取值于（rang over）函数的变量，和来自它们的粘合子（binder）；二阶lambda演算取值自类型，和来自它们的粘合子。 作为一个例子，恒等函数有形如A→ A的任何类型的事实可以在系统F中被形式化为判断 这里的α是。 在Curry-Howard同构下，系统F对应于二阶逻辑。 系统F，和甚至更加有表达力的lambda演算一起，可被看作Lambda立方体的一部分。 (zh)
|
| rdfs:comment
|
- Il sistema F, anche conosciuto come lambda calcolo polimorfico o lambda calcolo di secondo ordine, è un . È stato scoperto indipendentemente dal logico e dall'informatico . Il sistema F formalizza la nozione di polimorfismo parametrico nei linguaggi di programmazione e pone le basi per linguaggi come , ML, e . Come sistema di riscrittura di termini, è . (it)
- 系统F，也叫做多态lambda演算或二阶lambda演算，是有类型lambda演算。它由逻辑学家和计算机科学家独立发现的。系统F形式化了编程语言中的参数多态的概念。 正如同lambda演算有取值于（rang over）函数的变量，和来自它们的粘合子（binder）；二阶lambda演算取值自类型，和来自它们的粘合子。 作为一个例子，恒等函数有形如A→ A的任何类型的事实可以在系统F中被形式化为判断 这里的α是。 在Curry-Howard同构下，系统F对应于二阶逻辑。 系统F，和甚至更加有表达力的lambda演算一起，可被看作Lambda立方体的一部分。 (zh)
- To Σύστημα F, επίσης γνωστό ως πολυμορφικός λ-λογισμός των Ζιράρ-Ρέινολντς και λ-λογισμός δευτέρας τάξης, είναι ένας λ-λογισμός με τύπους που επεκτείνει τον λ-λογισμό με απλούς τύπους εισάγοντας ένα μηχανισμό καθολικής ποσόδειξης επί των τύπων. Ως εκ τούτου, το Σύστημα F αποτελεί φορμαλισμό της έννοιας του παραμετρικού πολυμορφισμού στις γλώσσες προγραμματισμού, και μια θεωρητική βάση γλωσσών όπως η Haskell και η ML. Το Σύστημα F επινοήθηκε ανεξάρτητα από τον και τον . (el)
- Le système F est un formalisme logique qui permet d'exprimer de façon très riche et très rigoureuse des fonctions et d'y démontrer formellement des propriétés difficiles. Plus précisément, 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'existence d'une quantification universelle sur les types qui permet d'exprimer du polymorphisme. (fr)
- System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphism in programming languages, thus forming a theoretical basis for languages such as Haskell and ML. It was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974). According to Girard, the "F" in System F was picked by chance. (en)
- System F（システム・エフ）は、型付きラムダ計算の一体系であり、単純型付きラムダ計算に、型についての全称量化を取り入れた計算機構である。二階ラムダ計算、ポリモーフィックラムダ計算とも言われる。プログラミング言語でのを形式化するもので、関数型言語のMLやHaskellなどの型システムのベース理論にされている。System Fは、論理学者のジャン＝イヴ・ジラールと計算機科学者のの両者が別個に発見している。ジラールによるとSystem Fの語源は、たまたまそう名付けただけと言う。 単純型付きラムダ計算では、関数についての変数とその束縛が存在するが、System Fでは型についての変数とその束縛が追加されている。例えば恒等関数は任意の型についての形の型を持ちうるが、System Fではこのことが次の判断が成り立つことによって表されている。 . ここで、はである。また、小文字のが通常の値レベルの抽象を表しているのに対して、大文字のを型レベルの抽象を表すために使用している。 (ja)
- 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. (pl)
- Система F (полиморфное лямбда-исчисление, система , типизированное лямбда-исчисление второго порядка) — система типизированного лямбда-исчисления, отличающаяся от просто типизированной системы наличием механизма универсальной квантификации над типами. Эту систему разработал в 1972 году Жан-Ив Жирар в контексте теории доказательств в логике. Независимо от него подобную систему предложил в 1974 году Джон Рейнольдс. Система F позволяет формализовать концепцию параметрического полиморфизма в языках программирования и служит теоретической основой для таких языков программирования как Haskell и ML. (ru)
|
