System F (original) (raw)
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, è .
| Property | Value |
|---|---|
| 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) |
| dbo:wikiPageExternalLink | http://www.PaulTaylor.EU/stable/Proofs%2BTypes.html http://www.macs.hw.ac.uk/~jbw/papers/Wells:Typability-and-Type-Checking-in-the-Second-Order-Lambda-Calculus-Are-Equivalent-and-Undecidable:LICS-1994.ps.gz http://www.site.uottawa.ca/~fbinard/Intuitionism/TypeTheory/SystemF/ https://kilthub.cmu.edu/articles/journal_contribution/Towards_a_Theory_of_Type_Structure/6611015/files/12103187.pdf https://books.google.com/books%3Fid=IL-SI67hjI4C&printsec=frontcover&dq=Nicolas+Bourbaki&source=bl&ots=nbfmxi9gJK&sig=4nPo8EFXrQYwAC2y0pD0uGv-EGY&hl=en&sa=X&ei=3sYBUOukIMLW2AX4t_inCw&ved=0CD8Q6AEwAg%23v=onepage&q=Nicolas%20Bourbaki&f=false https://books.google.com/books%3Fid=ti6zoAC9Ph8C&pg=PA340 https://web.archive.org/web/20140917015759/http:/www.eecs.harvard.edu/~greg/cs256sp2005/lec16.txt |
| dbo:wikiPageID | 767637 (xsd:integer) |
| dbo:wikiPageLength | 18468 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1123450918 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Typed_lambda_calculus dbr:Universal_quantification dbc:Lambda_calculus dbc:Logic dbr:Decision_problem dbr:Intuitionistic_logic dbr:ML_programming_language dbr:Glasgow_Haskell_Compiler dbr:ML_(programming_language) dbr:Simply_typed_lambda_calculus dbr:Statically_typed dbr:Computer_scientist dbr:Henk_Barendregt dbr:Dependent_types dbr:Parametric_polymorphism dbr:Programming_language_theory dbc:Polymorphism_(computer_science) dbc:1971_in_computing dbc:1974_in_computing dbr:Lambda_cube dbr:Church_encoding dbr:Kind_(type_theory) dbr:Record_(computer_science) dbr:Haskell_(programming_language) dbr:Higher-order_function dbr:Hindley–Milner dbr:Jean-Yves_Girard dbc:Type_theory dbr:John_C._Reynolds dbr:Greg_Morrisett dbr:Term_rewriting_system dbr:IEEE dbr:OCaml dbr:Type_inference dbr:Programming_language dbr:Subtyping dbr:Fixed-point_combinator dbr:System_U dbr:Logician dbr:Type_variable dbr:Normalization_property_(lambda-calculus) dbr:Church_numeral dbr:Martin-Löf's_type_theory dbr:Right-associative dbr:Functional_programming_languages dbr:Generalized_algebraic_data_types dbr:Curry–Howard_isomorphism dbr:Existential_types dbr:Type-checking dbr:Type_operator dbr:Joe_Wells |
| dbp:wikiPageUsesTemplate | dbt:Citation dbt:Citation_needed dbt:Cite_book dbt:Cite_conference dbt:Clear dbt:For dbt:Mono dbt:Mvar dbt:Refbegin dbt:Refend dbt:Reflist dbt:Short_description dbt:Wikibooks |
| dcterms:subject | dbc:Lambda_calculus dbc:Logic dbc:Polymorphism_(computer_science) dbc:1971_in_computing dbc:1974_in_computing dbc:Type_theory |
| 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) |
| rdfs:label | System F (en) Σύστημα F (el) Sistema F (it) Système F (fr) System F (ja) System F (pl) Система F (ru) Система F (uk) 系统F (zh) |
| owl:sameAs | freebase:System F wikidata:System F dbpedia-el:System F dbpedia-fr:System F dbpedia-hr:System F dbpedia-it:System F dbpedia-ja:System F dbpedia-pl:System F dbpedia-ru:System F dbpedia-uk:System F dbpedia-zh:System F https://global.dbpedia.org/id/2QPdr |
| prov:wasDerivedFrom | wikipedia-en:System_F?oldid=1123450918&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:System_F |
| is dbo:knownFor of | dbr:Jean-Yves_Girard dbr:John_C._Reynolds |
| is dbo:wikiPageRedirects of | dbr:System_F: dbr:System_FC dbr:System_Fω dbr:System_f dbr:System_F-sub dbr:F_omega dbr:Universal_types dbr:Girard-Reynolds_isomorphism dbr:Fω dbr:System_F-omega dbr:Cry_(System_F_song) dbr:Polymorphic_Lambda_Calculus dbr:Polymorphic_lambda_calculus dbr:Higher-order_polymorphic_lambda_calculus dbr:Second-order_lambda_calculus dbr:Second_order_lambda_calculus |
| is dbo:wikiPageWikiLink of | dbr:Categorical_logic dbr:School_of_Informatics,_University_of_Edinburgh dbr:List_of_computer_scientists dbr:Typed_lambda_calculus dbr:Dependent_type dbr:List_of_University_of_Edinburgh_people dbr:List_of_important_publications_in_computer_science dbr:Pegasus_in_popular_culture dbr:Per_Martin-Löf dbr:List_of_mathematical_logic_topics dbr:List_of_performers_on_Top_of_the_Pops dbr:List_of_programmers dbr:Normal_form_(abstract_rewriting) dbr:Giuseppe_Ottaviani dbr:Glasgow_Haskell_Compiler dbr:Bounded_quantifier dbr:System_F: dbr:System_FC dbr:System_Fω dbr:System_f dbr:Calculus_of_constructions dbr:Simply_typed_lambda_calculus dbr:Parametric_polymorphism dbr:Polymorphism_(computer_science) dbr:Programming_language_theory dbr:Total_functional_programming dbr:Type_system dbr:Type_theory dbr:Lambda_cube dbr:System_F-sub dbr:Curry–Howard_correspondence dbr:POPLmark_challenge dbr:Church_encoding dbr:Hindley–Milner_type_system dbr:Jean-Yves_Girard dbr:Takeuti's_conjecture dbr:John_C._Reynolds dbr:Lambda_calculus dbr:Mogensen–Scott_encoding dbr:F_omega dbr:Oakenfold_Anthems dbr:Rank_1 dbr:Meta-circular_evaluator dbr:Second-order_arithmetic dbr:Type_inhabitation dbr:Fixed-point_combinator dbr:System_U dbr:Universal_type dbr:Universal_types dbr:Second-order_propositional_logic dbr:Type_constructor dbr:Type_variable dbr:Turing_completeness dbr:Girard-Reynolds_isomorphism dbr:Fω dbr:System_F-omega dbr:Cry_(System_F_song) dbr:Polymorphic_Lambda_Calculus dbr:Polymorphic_lambda_calculus dbr:Higher-order_polymorphic_lambda_calculus dbr:Second-order_lambda_calculus dbr:Second_order_lambda_calculus |
| is dbp:knownFor of | dbr:Jean-Yves_Girard |
| is foaf:primaryTopic of | wikipedia-en:System_F |