Lambda cube (original) (raw)
Initialement proposé par Henk Barendregt, le -cube permet de visualiser les différentes dimensions pour lesquelles le calcul des constructions apporte une généralisation par rapport au lambda-calcul simplement typé où un terme ne peut dépendre que d'un autre terme. Chaque axe représente une nouvelle forme d'abstraction : * Terme dépendant de type : le polymorphisme ; * Type dépendant de type : présence d'opérateurs de types ; * Type dépendant de terme.
| Property | Value |
|---|---|
| dbo:abstract | In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to: * x-axis: types that can bind terms, corresponding to dependent types. * y-axis: terms that can bind types, corresponding to polymorphism. * z-axis: types that can bind types, corresponding to (binding) type operators. The different ways to combine these three dimensions yield the 8 vertices of the cube, each corresponding to a different kind of typed system. The λ-cube can be generalized into the concept of a pure type system. (en) Initialement proposé par Henk Barendregt, le -cube permet de visualiser les différentes dimensions pour lesquelles le calcul des constructions apporte une généralisation par rapport au lambda-calcul simplement typé où un terme ne peut dépendre que d'un autre terme. Chaque axe représente une nouvelle forme d'abstraction : * Terme dépendant de type : le polymorphisme ; * Type dépendant de type : présence d'opérateurs de types ; * Type dépendant de terme. (fr) 型理論において、ラムダ・キューブ (Lambda cube) とは、8つの異なる型付きラムダ計算の関係を表した図である。これらの計算体系がそれぞれ型（type）と項（term）の間にどのような依存関係を認めるかを整理したもので、単純型付きラムダ計算から、を導くフレームワークになっている。数学者ヘンク・バレンドレフトによって1991年に提唱された。 （右図参照）ラムダキューブの原点は、単純型付きラムダ計算に相当する。三つの座標軸は、Y軸=パラメトリック多相、Z軸=型オペレータ、X軸=依存型に対応している。X, Y, Zの三軸線を融合した終点のは、Calculus of Constructionsに相当する。 各頂点は、以下の通りである: λ→項に依存した項（単純型付きラムダ計算）一階命題論理（これを以下全てが含む。）λ2型に依存した項（System F）パラメトリック多相λω型に依存した型（System Fω）型オペレータ弱性λω型に依存した型、型に依存した項（System Fω）型構築子λ2とλωの融合λP項に依存した型（）依存型一階述語論理λP2型に依存した項、項に依存した型（）依存型二階述語論理λPとλ2の融合λPω項に依存した型、型に依存した型（）依存型弱性高階述語論理λPとλωの融合λC型に依存した型、型に依存した項、項に依存した型（）CoC高階述語論理λP2とλPωの融合 (ja) Ля́мбда-куб (λ-куб) — наглядная классификация восьми типизированных лямбда-исчислений с явным приписыванием типов (систем, типизированных по Чёрчу). Куб организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею λ-куба предложил в 1991 году нидерландский логик и математик Хенк Барендрегт. Дальнейшие обобщения лямбда-куба можно получить, рассматривая чистую систему типов. (ru) Ля́мбда-куб (λ-куб) — наочна класифікація восьми типізованих лямбда-числень з явним приписуванням типів (систем, типізованих за Черчем). Куб організований відповідно до можливих залежностей між типами і термами цього числення і формує природну структуру для числення конструкцій. Ідею λ-куба запропонував 1991 року нідерландський логік і математик Генк Барендрегт. Подальші узагальнення лямбда-куба можна отримати, розглядаючи чисту систему типів. (uk) 在数理逻辑和类型论中，λ-立方是探索 的构造演算中细化轴的框架，以简单类型 λ-演算（在立方图中写作 λ→）作为原点放在立方体的顶点，而构造演算（即高阶依赖类型化 λ-演算，在图中写作 λPω）则是其空间对顶点。立方体的每个轴都表示一种新的抽象形式： * 值依赖类型，或多态。系统F，即二阶λ-演算（图中写作 λ2）就是通过只加入此性质得到的。 * 类型依赖类型，或类型构造器。带类型构造器的简单类型 λ-演算（图中为）就是通过只加入此性质得到的。它与系统F结合就产生了系统Fω（在图中写作不带下划线的λω）。 * 类型依赖值，或依赖类型。只加入此性质就得到了λΠ（在图中写作λP），一种与LF紧密相关的类型系统。 所有的八种演算包含了最基本的抽象形式，值依赖值即简单类型 λ-演算中的普通函数。此立方中最丰富的演算即构造演算，它带有所有三种抽象。所有八种演算都是强规范化的。 然而子类型并未展示在此立方中，尽管像 这样以闻名的，结合了子类型和多态的系统具有实际意义，它可被进一步推广为。进一步扩展到允许的定义；这些系统通常在λ-立方的论文发表后才被开发出来。 此立方的思想来源于Henk Barendregt (1991)。就此立方的所有角而言，的框架涵盖了λ-立方，其它一些系统也可表示为此通用框架的实例。 此框架的出现比λ-立方早上几年。在 Barendregt 1991年的论文中，他也在此框架中定义了λ-立方的角。 Olivier Ridoux 在他的 Habilitation à diriger les recherches Lambda-Prolog de A à Z... ou presque 中给出了此立方的一个截边角后的模版(p. 70) 的两种表示，一种将此立方表示为一个八面体，其中 8 个顶点以面代替，另一种将它表示为一个十二面体，其中 12 条棱则以面代替。 (zh) |
| dbo:thumbnail | wiki-commons:Special:FilePath/Lambda_Cube_img.svg?width=300 |
| dbo:wikiPageExternalLink | http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm https://www.microsoft.com/en-us/research/wp-content/uploads/1997/01/henk.pdf |
| dbo:wikiPageID | 901593 (xsd:integer) |
| dbo:wikiPageLength | 20631 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1070547606 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Propositional_calculus dbr:Dependent_type dbc:Lambda_calculus dbr:Homotopy_type_theory dbr:Peano_arithmetic dbr:Mathematical_logic dbr:Free_variables_and_bound_variables dbr:Reflexive_transitive_closure dbr:ML_(programming_language) dbr:Calculus_of_constructions dbr:Simply_typed_lambda_calculus dbr:Henk_Barendregt dbr:Dependent_types dbr:Parametric_polymorphism dbr:Pure_type_system dbr:Type_theory dbr:First-order_logic dbr:Logical_framework dbr:Subject_reduction dbc:Type_theory dbr:Higher-order_logic dbr:System_F dbr:Automath dbr:Typing_rule dbr:Impredicativity dbr:OCaml dbr:Church-Rosser_property dbr:Subtyping dbr:Second-order_propositional_logic dbr:Type_constructor dbr:Β-reduction dbr:Predicate_Logic dbr:System_F-omega dbr:Impredicative dbr:Pure_type_systems dbr:Simply_typed_λ-calculus dbr:Second_order_predicate_calculus dbr:Curry_Howard_isomorphism dbr:ΛΠ-calculus dbr:Type_operator dbr:Bounded_type_operator dbr:File:Lambda_Cube_img.svg dbr:Higher-order_bounded_quantification dbr:Purely_functional_objects |
| dbp:wikiPageUsesTemplate | dbt:Cite_web dbt:Cleanup_rewrite dbt:Na dbt:Reflist dbt:Rp dbt:Underline dbt:Ya |
| dct:subject | dbc:Lambda_calculus dbc:Type_theory |
| rdfs:comment | Initialement proposé par Henk Barendregt, le -cube permet de visualiser les différentes dimensions pour lesquelles le calcul des constructions apporte une généralisation par rapport au lambda-calcul simplement typé où un terme ne peut dépendre que d'un autre terme. Chaque axe représente une nouvelle forme d'abstraction : * Terme dépendant de type : le polymorphisme ; * Type dépendant de type : présence d'opérateurs de types ; * Type dépendant de terme. (fr) 型理論において、ラムダ・キューブ (Lambda cube) とは、8つの異なる型付きラムダ計算の関係を表した図である。これらの計算体系がそれぞれ型（type）と項（term）の間にどのような依存関係を認めるかを整理したもので、単純型付きラムダ計算から、を導くフレームワークになっている。数学者ヘンク・バレンドレフトによって1991年に提唱された。 （右図参照）ラムダキューブの原点は、単純型付きラムダ計算に相当する。三つの座標軸は、Y軸=パラメトリック多相、Z軸=型オペレータ、X軸=依存型に対応している。X, Y, Zの三軸線を融合した終点のは、Calculus of Constructionsに相当する。 各頂点は、以下の通りである: λ→項に依存した項（単純型付きラムダ計算）一階命題論理（これを以下全てが含む。）λ2型に依存した項（System F）パラメトリック多相λω型に依存した型（System Fω）型オペレータ弱性λω型に依存した型、型に依存した項（System Fω）型構築子λ2とλωの融合λP項に依存した型（）依存型一階述語論理λP2型に依存した項、項に依存した型（）依存型二階述語論理λPとλ2の融合λPω項に依存した型、型に依存した型（）依存型弱性高階述語論理λPとλωの融合λC型に依存した型、型に依存した項、項に依存した型（）CoC高階述語論理λP2とλPωの融合 (ja) Ля́мбда-куб (λ-куб) — наглядная классификация восьми типизированных лямбда-исчислений с явным приписыванием типов (систем, типизированных по Чёрчу). Куб организован в соответствии с возможными зависимостями между типами и термами этого исчисления и формирует естественную структуру для исчисления конструкций. Идею λ-куба предложил в 1991 году нидерландский логик и математик Хенк Барендрегт. Дальнейшие обобщения лямбда-куба можно получить, рассматривая чистую систему типов. (ru) Ля́мбда-куб (λ-куб) — наочна класифікація восьми типізованих лямбда-числень з явним приписуванням типів (систем, типізованих за Черчем). Куб організований відповідно до можливих залежностей між типами і термами цього числення і формує природну структуру для числення конструкцій. Ідею λ-куба запропонував 1991 року нідерландський логік і математик Генк Барендрегт. Подальші узагальнення лямбда-куба можна отримати, розглядаючи чисту систему типів. (uk) In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to: (en) 在数理逻辑和类型论中，λ-立方是探索 的构造演算中细化轴的框架，以简单类型 λ-演算（在立方图中写作 λ→）作为原点放在立方体的顶点，而构造演算（即高阶依赖类型化 λ-演算，在图中写作 λPω）则是其空间对顶点。立方体的每个轴都表示一种新的抽象形式： * 值依赖类型，或多态。系统F，即二阶λ-演算（图中写作 λ2）就是通过只加入此性质得到的。 * 类型依赖类型，或类型构造器。带类型构造器的简单类型 λ-演算（图中为）就是通过只加入此性质得到的。它与系统F结合就产生了系统Fω（在图中写作不带下划线的λω）。 * 类型依赖值，或依赖类型。只加入此性质就得到了λΠ（在图中写作λP），一种与LF紧密相关的类型系统。 所有的八种演算包含了最基本的抽象形式，值依赖值即简单类型 λ-演算中的普通函数。此立方中最丰富的演算即构造演算，它带有所有三种抽象。所有八种演算都是强规范化的。 然而子类型并未展示在此立方中，尽管像 这样以闻名的，结合了子类型和多态的系统具有实际意义，它可被进一步推广为。进一步扩展到允许的定义；这些系统通常在λ-立方的论文发表后才被开发出来。 (zh) |
| rdfs:label | Lambda cube (en) Lambda cube (fr) ラムダ・キューブ (ja) Лямбда-куб (ru) Lambda立方体 (zh) Лямбда-куб (uk) |
| owl:sameAs | freebase:Lambda cube wikidata:Lambda cube dbpedia-fr:Lambda cube dbpedia-ja:Lambda cube dbpedia-ru:Lambda cube dbpedia-uk:Lambda cube dbpedia-zh:Lambda cube https://global.dbpedia.org/id/vqKn |
| prov:wasDerivedFrom | wikipedia-en:Lambda_cube?oldid=1070547606&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Lambda_Cube_img.svg |
| foaf:isPrimaryTopicOf | wikipedia-en:Lambda_cube |
| is dbo:wikiPageDisambiguates of | dbr:Cube_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:Lambda-cube dbr:Barendregt_cube dbr:Λ-cube dbr:Λ_cube |
| is dbo:wikiPageWikiLink of | dbr:Typed_lambda_calculus dbr:Dependent_type dbr:List_of_mathematical_logic_topics dbr:Calculus_of_constructions dbr:Parametric_polymorphism dbr:Pure_type_system dbr:Type_theory dbr:Cube_(disambiguation) dbr:History_of_type_theory dbr:Natural_deduction dbr:Lambda_calculus dbr:Mogensen–Scott_encoding dbr:System_F dbr:Type_constructor dbr:Lambda-cube dbr:Barendregt_cube dbr:Λ-cube dbr:Λ_cube |
| is owl:differentFrom of | dbr:Logical_cube |
| is foaf:primaryTopic of | wikipedia-en:Lambda_cube |
