A typed lambda calculus is a typed formalism that uses the lambda-symbol (<math>\lambda</math>) 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).

PropertyValue
dbpprop:abstract
  • A typed lambda calculus is a typed formalism that uses the lambda-symbol (<math>\lambda</math>) 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).
  • 型付きラムダ計算（英: typed lambda calculus）とは、無名の関数の抽象表現にラムダ (<math>\lambda</math>) というシンボルを用いる型付き形式手法である。型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskell型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。 ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。 様々な型付きラムダ計算がこれまで研究されてきた。単純型付きラムダ計算はいくつかの基本型（または型変数）と関数型 <math>\sigma\to\tau</math> から成る。System T はこれを拡張し、自然数型と高階原始再帰を加えたものである。この系ではペアノ算術において全ての再帰する可能性のある関数が定義可能である。System F は、全ての型に対して全称量化を施すことでポリモーフィズムを実現している。これを論理学的に見れば、二階述語論理に属する全ての関数を記述できることを意味する。依存型のあるラムダ計算は直観主義的型理論の基盤であり、calculus of constructions や logical framework (LF) の基盤である。Berardi の成果に基づき Barendregt が提案したラムダ・キューブは、純粋な型付きラムダ計算（単純型付きラムダ計算、System F、LF、calculus of constructions など）の関係を体系化したものである。 一部の型付きラムダ計算には「派生型」の記法が導入されている。すなわち、<math>A</math> が <math>B</math> の派生型であるとき、型が <math>A</math> である全ての項は型が <math>B</math> でもある。派生型のある型付きラムダ計算は単に普通の型付きラムダ計算に結合型 (conjunctive type) と <math>F^\leq</math> (F-sub) を加えたものである。 以上の体系はすべて（型のないラムダ計算以外）、「強く正規化 (strongly normalizing)」する。すなわち、全ての計算は停止する。結果としてそれらは論理として一貫しており、uninhabited types がある。しかし、強く正規化しない型付きラムダ計算も存在する。全ての型の型 を持つ依存型付きラムダ計算は Girard's paradox により正規化しない。この系は最も単純な純粋型システムでもあり、ラムダ・キューブを一般化した形式手法である。明示的な再帰コンビネータを持つ系（Gordon Plotkin の PCF など）も正規化しないが、論理体系として解釈されることを意図していない。実際、PCF は型付き関数型プログラミング言語であり、型はプログラムが正しく動作することを保証する目的で使われているが、必ずしも停止を保証しない。 型付きラムダ計算はプログラミング言語の新たな型システムの設計で重要な役割を演じている。型付け可能性は一般にプログラミングの好ましい属性を捉え、例えば、プログラムがメモリアクセス違反を起こさないようにするといったことが考えられる。 プログラミングにおいて、強い型付けのプログラミング言語のルーチン（関数、プロシージャ、メソッド）は、型付きラムダ計算と密接に関連している。Eiffelには "inline agent" の記法があり、型付きラムダ式を直接定義して操作できる。例えば、agent : STRING do Result := p. spouse. name end という式があるとき、これはある人 (person) の配偶者 (spouse) の名前を返す関数を表したオブジェクトを記述している。
  • Типизированное λ-исчисление — это ти́повый формализм, использующий символ абстракции «λ» для записи выражений, обозначающих безымянные функции. Типовые λ-исчисления являются фундаментальными примитивными языками программирования, которые обеспечивают основу типовым языкам функционального программирования — аппликативным языкам, — среди которых ML и Haskell, а также типовым императивным языкам программирования. λ-исчисление с типами является языком декартово-замкнутой категории, что устанавливает прямую связь с такой моделью вычислений, как категориальная абстрактная машина. С одной точки зрения типовые λ-исчисления могут рассматриваться как специализации бестиповых λ-исчислений, а с другой — наоборот, типовые языки могут считаться более фундаментальными, из которых бестиповые получаются как частные случаи. Анализ этого явления дает теория вычислений Д. Скотта. λ-исчисление с типами служит основой для разработки новых систем типизации для языков программирования, поскольку именно средствами типов и зависимостей между ними выражаются желаемые свойства программ. В программировании самостоятельные вычислительные блоки (функции, процедуры, методы) языков программирования с сильной типизацией соответствуют типовым λ-выражениям.
  • 有类型 lambda 演算是使用 lambda 符号（<math>\lambda</math>）指示匿名函数抽象的一种有类型的形式化。有类型 lambda 演算是基础编程语言并且是有类型的函数式编程语言如 ML 和 Haskell 和更间接的指令式编程语言的基础。它们通过 Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言，比如简单类型 lambda 演算是笛卡尔闭范畴（CCC）的语言。 传统上，有类型 lambda 演算被看作无类型lambda演算的精细化。更现代的观点把有类型 lambda 演算看做更基础的理论，而把无类型 lambda 演算看作它的只有一个类型的特殊情况。
dbpprop:date
  • August 2009
dbpprop:hasPhotoCollection
dbpprop:wikiPageUsesTemplate
rdfs:comment
  • A typed lambda calculus is a typed formalism that uses the lambda-symbol (<math>\lambda</math>) 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).
  • Типизированное λ-исчисление — это ти́повый формализм, использующий символ абстракции «λ» для записи выражений, обозначающих безымянные функции.
rdfs:label
  • Typed lambda calculus
  • 型付きラムダ計算
  • Типизированное лямбда-исчисление
  • 有类型lambda演算
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of