Typed lambda calculus (original) (raw)
Rachunek lambda z typami to postać rachunku lambda rozszerzona o typy i z ograniczeniami,jakie wyrażenia są dozwolone, zależnie od ich typów. Najprostszym takim rachunkiem jest .
| Property | Value |
|---|---|
| dbo:abstract | Ο λ-λογισμός με τύπους είναι ένας τυποποιημένος φορμαλισμός που χρησιμοποιεί το σύμβολο λ για την ανώνυμη αφαίρεση συνάρτησης. Σε αυτό το πλαίσιο, οι τύποι συνήθως είναι αντικείμενα συντακτικής φύσης που αντιστοιχίζονται σε λ-όρους - η ακριβής φύση ενός τύπου εξαρτάται από τον εκάστοτε λογισμό (βλ. παρακάτω). Οι λ-λογισμοί με τύπους μπορούν να θεωρηθούν εκλεπτυσμένες εκδόσεις του αλλά μπορούν επίσης να θεωρηθούν και σαν βασικότερη θεωρία, με τον λ-λογισμό χωρίς τύπους να είναι ειδική περίπτωση που έχει μόνο έναν τύπο. Οι λ-λογισμοί με τύπους είναι θεμελιώδεις γλώσσες προγραμματισμου και αποτελούν τη βάση των γλωσσών συναρτησιακού προγραμματισμού με τύπους όπως η ML και η Haskell, και κάπως γενικότερα των γλωσσών προστακτικού προγραμματισμού. Οι λ-λογισμοί με τύπους παίζουν σημαντικό ρόλο στη σχεδίαση των συστημάτων τύπων των γλωσσών προγραμματισμού, όπου η τυποποιησιμότητα συνήθως εκφράζει επιθυμητές ιδιότητες του προγράμματος, όπως π.χ. ότι το πρόγραμμα δε θα προκαλέσει κάποιο σφάλμα μνήμης. Οι λ-λογισμοί με τύπους έχουν στενή σχέση με τη μαθηματική λογική και τη μέσω του και μπορούν να θεωρηθούν η εσωτερική γλώσσα των κλάσεων των κατηγοριών, π.χ. ο λ-λογισμός με απλούς τύπους είναι η γλώσσα των καρτεσιανά κλειστών κατηγοριών. (el) A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see kinds below). From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus, but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type. Typed lambda calculi are foundational programming languages and are the base of typed functional programming languages such as ML and Haskell and, more indirectly, typed imperative programming languages. Typed lambda calculi play an important role in the design of type systems for programming languages; here, typability usually captures desirable properties of the program (e.g., the program will not cause a memory access violation). Typed lambda calculi are closely related to mathematical logic and proof theory via the Curry–Howard isomorphism and they can be considered as the internal language of classes of categories; e.g., the simply typed lambda calculus is the language of Cartesian closed categories (CCCs). (en) 型付きラムダ計算（英: typed lambda calculus）とは、無名の関数の抽象表現にラムダ というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。 ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。 様々な型付きラムダ計算がこれまで研究されてきた。単純型付きラムダ計算はいくつかの基本型（または型変数）と関数型 から成る。 はこれを拡張し、自然数型と高階原始再帰を加えたものである。この系ではペアノ算術において全ての再帰する可能性のある関数が定義可能である。System F は、全ての型に対して全称量化を施すことでポリモーフィズムを実現している。これを論理学的に見れば、二階述語論理に属する全ての関数を記述できることを意味する。依存型のあるラムダ計算はの基盤であり、calculus of constructions や logical framework (LF) の基盤である。Berardi の成果に基づき Barendregt が提案したラムダ・キューブは、純粋な型付きラムダ計算（単純型付きラムダ計算、System F、LF、calculus of constructions など）の関係を体系化したものである。 一部の型付きラムダ計算には「サブタイピング」の概念が導入されている。すなわち、 が のサブタイプ（下位型）であるとき、型の項は必ず型の項でもある。サブタイピングのある型付きラムダ計算としては、単純型付きラムダ計算に conjunctive type を加えたものと (F<:) が挙げられる。 以上の体系はすべて（型のないラムダ計算以外）、「強く正規化 (strongly normalizing)」する。すなわち、全ての計算は停止する。結果としてそれらは論理として一貫しており、uninhabited types がある。しかし、強く正規化しない型付きラムダ計算も存在する。全ての型の型 (Type : Type) を持つ依存型付きラムダ計算は Girard's paradox により正規化しない。この系は最も単純なでもあり、ラムダ・キューブを一般化した形式手法である。明示的な再帰コンビネータを持つ系（Gordon Plotkin の PCF など）も正規化しないが、論理体系として解釈されることを意図していない。実際、PCF (Programming language for Computable Functions) は型付き関数型プログラミング言語であり、型はプログラムが正しく動作することを保証する目的で使われているが、必ずしも停止を保証しない。 型付きラムダ計算はプログラミング言語の新たな型システムの設計で重要な役割を演じている。型付け可能性は一般にプログラミングの好ましい属性を捉え、例えば、プログラムがメモリアクセス違反を起こさないようにするといったことが考えられる。 プログラミングにおいて、強い型付けのプログラミング言語のルーチン（関数、プロシージャ、メソッド）は、型付きラムダ計算と密接に関連している。Eiffelには "inline agent" の記法があり、型付きラムダ式を直接定義して操作できる。例えば、agent (p: PERSON): STRING do Result := p.spouse.name end という式があるとき、これはある人 (person) の配偶者 (spouse) の名前を返す関数を表したオブジェクトを記述している。 (ja) Типизированное лямбда-исчисление — это версия лямбда-исчисления, в которой лямбда-термам приписываются специальные синтаксические метки, называемые типами. Допустимы различные наборы правил конструирования и приписывания таких меток, они порождают различные системы типизации. Типовые -исчисления являются фундаментальными примитивными языками программирования, которые обеспечивают основу типовым языкам функционального программирования — аппликативным языкам, — среди которых ML и Haskell, а также типовым императивным языкам программирования. -исчисление с типами является языком декартово-замкнутой категории, что устанавливает прямую связь с такой моделью вычислений, как категориальная абстрактная машина. С одной точки зрения типовые -исчисления могут рассматриваться как специализации бестиповых -исчислений, а с другой — наоборот, типовые языки могут считаться более фундаментальными, из которых бестиповые получаются как частные случаи. Анализ этого явления дает теория вычислений Д. Скотта. -исчисление с типами служит основой для разработки новых для языков программирования, поскольку именно средствами типов и зависимостей между ними выражаются желаемые свойства программ. В программировании самостоятельные вычислительные блоки (функции, процедуры, методы) языков программирования с сильной типизацией соответствуют типовым -выражениям. (ru) Rachunek lambda z typami to postać rachunku lambda rozszerzona o typy i z ograniczeniami,jakie wyrażenia są dozwolone, zależnie od ich typów. Najprostszym takim rachunkiem jest . (pl) Типізоване лямбда-числення — це система лямбда-числення, у якій кожний вислів має тип. У цьому контексті тип — це формула певної системи числення, як-от (інтуїціоністської) пропозиційної логіки або логіки першого порядку. Типізоване Лямбда-числення з простими типами (де типи — це формули імплікаційного фрагменту інтуїціоністської логіки) має застосування на практиці в функціональних мовах програмування, як от Haskell. Складніші типізовані системи є важливими для вивчення загальних характеристик обчислюваності та у сфері автоматиції автоматичних доведень. (uk) 有类型lambda演算是使用lambda符号（）指示匿名函数抽象的一种有类型的形式化。有类型lambda演算是基础编程语言并且是有类型的函数式编程语言如ML和Haskell和更间接的指令式编程语言的基础。它们通过Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言，比如简单类型lambda演算是笛卡尔闭范畴（CCC）的语言。 传统上，有类型lambda演算被看作无类型lambda演算的精细化。更现代的观点把有类型lambda演算看做更基础的理论，而把无类型lambda演算看作它的只有一个类型的特殊情况。 (zh) |
| dbo:wikiPageExternalLink | https://hbr.github.io/Lambda-Calculus/cc-tex https://ftp.science.ru.nl/CSI/CompMath.Found/HBK.ps |
| dbo:wikiPageID | 366208 (xsd:integer) |
| dbo:wikiPageLength | 5321 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1113070669 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Programming_languages dbc:Lambda_calculus dbr:Peano_arithmetic dbr:Intuitionistic_type_theory dbr:ML_programming_language dbr:Mathematical_logic dbr:Gordon_Plotkin dbr:Calculus_of_constructions dbr:Simply_typed_lambda_calculus dbr:Computer_programming dbr:Function_type dbr:Henk_Barendregt dbr:Dependent_types dbr:Pure_type_system dbr:Girard's_paradox dbr:Lambda_cube dbr:System_F-sub dbr:Dialectica_interpretation dbr:Kappa_calculus dbr:Proof_theory dbr:Haskell_(programming_language) dbc:Logic_in_computer_science dbc:Theory_of_computation dbc:Type_theory dbr:LF_(logical_framework) dbr:Lambda_calculus dbr:System_F dbr:Cartesian_closed_category dbr:Category_theory dbr:Second-order_logic dbr:Untyped_lambda_calculus dbr:Imperative_programming dbr:Formalism_(mathematics) dbr:Subtyping dbr:Internal_language dbr:Type_constructor dbr:Strongly_typed_programming_language dbr:Basic_type dbr:Turing-computable dbr:Strongly_normalizing dbr:Functional_programming_languages dbr:Programming_language_for_Computable_Functions dbr:Curry–Howard_isomorphism dbr:Type_systems |
| dbp:wikiPageUsesTemplate | dbt:Citation_needed dbt:Cite_book dbt:More_references |
| dcterms:subject | dbc:Lambda_calculus dbc:Logic_in_computer_science dbc:Theory_of_computation dbc:Type_theory |
| rdfs:comment | Rachunek lambda z typami to postać rachunku lambda rozszerzona o typy i z ograniczeniami,jakie wyrażenia są dozwolone, zależnie od ich typów. Najprostszym takim rachunkiem jest . (pl) Типізоване лямбда-числення — це система лямбда-числення, у якій кожний вислів має тип. У цьому контексті тип — це формула певної системи числення, як-от (інтуїціоністської) пропозиційної логіки або логіки першого порядку. Типізоване Лямбда-числення з простими типами (де типи — це формули імплікаційного фрагменту інтуїціоністської логіки) має застосування на практиці в функціональних мовах програмування, як от Haskell. Складніші типізовані системи є важливими для вивчення загальних характеристик обчислюваності та у сфері автоматиції автоматичних доведень. (uk) 有类型lambda演算是使用lambda符号（）指示匿名函数抽象的一种有类型的形式化。有类型lambda演算是基础编程语言并且是有类型的函数式编程语言如ML和Haskell和更间接的指令式编程语言的基础。它们通过Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言，比如简单类型lambda演算是笛卡尔闭范畴（CCC）的语言。 传统上，有类型lambda演算被看作无类型lambda演算的精细化。更现代的观点把有类型lambda演算看做更基础的理论，而把无类型lambda演算看作它的只有一个类型的特殊情况。 (zh) Ο λ-λογισμός με τύπους είναι ένας τυποποιημένος φορμαλισμός που χρησιμοποιεί το σύμβολο λ για την ανώνυμη αφαίρεση συνάρτησης. Σε αυτό το πλαίσιο, οι τύποι συνήθως είναι αντικείμενα συντακτικής φύσης που αντιστοιχίζονται σε λ-όρους - η ακριβής φύση ενός τύπου εξαρτάται από τον εκάστοτε λογισμό (βλ. παρακάτω). Οι λ-λογισμοί με τύπους μπορούν να θεωρηθούν εκλεπτυσμένες εκδόσεις του αλλά μπορούν επίσης να θεωρηθούν και σαν βασικότερη θεωρία, με τον λ-λογισμό χωρίς τύπους να είναι ειδική περίπτωση που έχει μόνο έναν τύπο. (el) A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered (see kinds below). From a certain point of view, typed lambda calculi can be seen as refinements of the untyped lambda calculus, but from another point of view, they can also be considered the more fundamental theory and untyped lambda calculus a special case with only one type. (en) 型付きラムダ計算（英: typed lambda calculus）とは、無名の関数の抽象表現にラムダ というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。 ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。 一部の型付きラムダ計算には「サブタイピング」の概念が導入されている。すなわち、 が のサブタイプ（下位型）であるとき、型の項は必ず型の項でもある。サブタイピングのある型付きラムダ計算としては、単純型付きラムダ計算に conjunctive type を加えたものと (F<:) が挙げられる。 (ja) Типизированное лямбда-исчисление — это версия лямбда-исчисления, в которой лямбда-термам приписываются специальные синтаксические метки, называемые типами. Допустимы различные наборы правил конструирования и приписывания таких меток, они порождают различные системы типизации. Типовые -исчисления являются фундаментальными примитивными языками программирования, которые обеспечивают основу типовым языкам функционального программирования — аппликативным языкам, — среди которых ML и Haskell, а также типовым императивным языкам программирования. (ru) |
| rdfs:label | Λ-λογισμός με τύπους (el) 型付きラムダ計算 (ja) Rachunek lambda z typami (pl) Типизированное лямбда-исчисление (ru) Typed lambda calculus (en) Типізоване лямбда-числення (uk) 有类型λ演算 (zh) |
| owl:sameAs | freebase:Typed lambda calculus wikidata:Typed lambda calculus dbpedia-el:Typed lambda calculus dbpedia-hr:Typed lambda calculus dbpedia-is:Typed lambda calculus dbpedia-ja:Typed lambda calculus dbpedia-pl:Typed lambda calculus dbpedia-ru:Typed lambda calculus dbpedia-uk:Typed lambda calculus dbpedia-zh:Typed lambda calculus https://global.dbpedia.org/id/2Spph |
| prov:wasDerivedFrom | wikipedia-en:Typed_lambda_calculus?oldid=1113070669&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Typed_lambda_calculus |
| is dbo:wikiPageRedirects of | dbr:Typed_lambda_calculi |
| is dbo:wikiPageWikiLink of | dbr:Programming_Computable_Functions dbr:List_of_functional_programming_topics dbr:Dependent_type dbr:Deductive_lambda_calculus dbr:Intuitionistic_type_theory dbr:List_of_mathematical_logic_topics dbr:Constructivism_(philosophy_of_mathematics) dbr:Escuela_Superior_Latinoamericana_de_Informática dbr:Normal_form_(abstract_rewriting) dbr:Epigram_(programming_language) dbr:Function_(mathematics) dbr:Bounded_quantifier dbr:Calculus_of_constructions dbr:Simply_typed_lambda_calculus dbr:Functional_programming dbr:Parametric_polymorphism dbr:Pure_type_system dbr:Böhm_tree dbr:Type_system dbr:Type_theory dbr:Curry–Howard_correspondence dbr:History_of_logic dbr:Proof_theory dbr:Higher-order_function dbr:Lambda_calculus dbr:Higher-order_logic dbr:Realizability dbr:System_F dbr:Automath dbr:Categorical_abstract_machine dbr:Meta-circular_evaluator dbr:Turnstile_(symbol) dbr:List_of_unsolved_problems_in_computer_science dbr:Fixed-point_combinator dbr:System_U dbr:Nonelementary_problem dbr:Phase_distinction dbr:ΛProlog dbr:Type_constructor dbr:Transparent_intensional_logic dbr:Typed_lambda_calculi |
| is foaf:primaryTopic of | wikipedia-en:Typed_lambda_calculus |