「型付きラムダ計算」の版間の差分

履歴の双方向閲覧

← 古い編集新しい編集 →

削除された内容追加された内容

ビジュアルウィキテキスト

インライン

2013年12月21日 (土) 07:23時点における版

型付きラムダ計算（かたつきらむだけいさん、英: typed lambda calculus）とは、定義域と値域の定まった関数を意味する型付きラムダ式と簡約規則からなる簡約の体系を言う。

定義

型付きラムダ式（typed lambda expression）

D, D' を集合または類（class）^[1]とする。M を D 上の値を取るものとする。このとき、

λ x : D' . M

は D' から D へのなにか写像（関数）f : D' → D を意味するものとする。このような λ を用いた関数の表現を型付きラムダ式（typed lambda expression）と呼ぶ。

さらに、D' の値を取る N に対して、(λ x : D' . M)N は一般的な関数でいうところの f(N) を意味するものとする。

脚注

^ フォンノイマン・ベルナイス・ゲーデル集合論の意味での類である。

参考文献

Joseph E. Stoy (1977). Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press
Alfred Tarski (1955), A lattice-theoretical fixpoint theorem and its applications
Dana Scott (1972), “Continuous lattices”, Lecture Notes in Mathematics Volume 274
Dana Scott (1976), “Data types as lattices”, Lecture Notes in Mathematics Volume 499
Henk Barendregt (1992). “Typed lambda calculi with types”. Handbook of Logic in Computer Science. Volume II. Oxford University Press

[1] フォンノイマン・ベルナイス・ゲーデル集合論の意味での類である。

[1]

@@ 1行目: / 1行目: @@
+'''型付きラムダ計算'''（かたつきらむだけいさん、{{lang-en-short|typed lambda calculus}}）とは、定義域と値域の定まった関数を意味する型付きラムダ式と簡約規則からなる簡約の体系を言う。
-'''型付きラムダ計算'''（{{lang-en-short|typed lambda calculus}}）とは、無名の関数の抽象表現にラムダ (<math>\lambda</math>) というシンボルを用いる型付き[[形式手法]]である。型付きラムダ計算は基礎的な[[プログラミング言語]]でもあり、[[ML (プログラミング言語)|ML]]や[[Haskell]]などの型付き[[関数型言語]]の基盤であり、さらには型付き[[命令型プログラミング]]言語の間接的な基盤とも言える。また、[[カリー・ハワード同型対応]]によって[[数理論理学]]と[[証明論]]とも密接に関連しており、[[圏論]]のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算は[[デカルト閉圏]] (CCC) の言語である。
+== 定義 ==
+=== 型付きラムダ式（typed lambda expression） ===
+D, D' を集合または類（class）<ref>フォンノイマン・ベルナイス・ゲーデル集合論の意味での類である。</ref>とする。M を D 上の値を取るものとする。このとき、
+:λ x : D' . M
+は D' から D へのなにか写像（関数）f : D' → D を意味するものとする。このような λ を用いた関数の表現を'''型付きラムダ式'''（typed lambda expression）と呼ぶ。
+さらに、D' の値を取る N に対して、(λ x : D' . M)N は一般的な関数でいうところの f(N) を意味するものとする。
+<!-- 何を言っているのか意味が分からないため
+== 概要 ==
+型付きラムダ計算は基礎的な[[プログラミング言語]]でもあり、[[ML (プログラミング言語)|ML]]や[[Haskell]]などの型付き[[関数型言語]]の基盤であり、さらには型付き[[命令型プログラミング]]言語の間接的な基盤とも言える。また、[[カリー・ハワード同型対応]]によって[[数理論理学]]と[[証明論]]とも密接に関連しており、[[圏論]]のクラスの内部言語と見なすこともできる。例えば単純な型付きラムダ計算は[[デカルト閉圏]] (CCC) の言語である。
 ある観点から見れば、型付きラムダ計算は型を持たない[[ラムダ計算]]を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。
@@ 12行目: / 22行目: @@
 [[プログラミング (コンピュータ)|プログラミング]]において、[[型システム#強い型付けと弱い型付け|強い型付け]]のプログラミング言語のルーチン（関数、プロシージャ、メソッド）は、型付きラムダ計算と密接に関連している。[[Eiffel]]には "inline agent" の記法があり、型付きラムダ式を直接定義して操作できる。例えば、'''agent''' (p: PERSON): STRING '''do Result''' := p.spouse.name '''end''' という式があるとき、これはある人 (person) の配偶者 (spouse) の名前を返す関数を表したオブジェクトを記述している。
+-->
+== 脚注 ==
+<references />
 == 参考文献 ==
+* {{cite book| author=Joseph E. Stoy| title=Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics|publisher=MIT Press | year=1977| }}
-* Henk Barendregt, [ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps Lambda Calculi with Types], Handbook of Logic in Computer Science, Volume II, Oxford University Press.
+* {{citation | author=Alfred Tarski | title=A lattice-theoretical fixpoint theorem and its applications | year=1955 | url=http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdf_1&handle=euclid.pjm/1103044538 | ref=Tarski(1955) }}
+* {{citation | author=Dana Scott | title=Continuous lattices | year=1972 | url=http://repository.readscheme.org/ftp/papers/plsemantics/oxford/Scott-PRG07.pdf | journal=Lecture Notes in Mathematics Volume 274 | ref=Scott(1972) }}
+* {{citation | author=Dana Scott | title=Data types as lattices | year=1976 | journal=Lecture Notes in Mathematics Volume 499 | url=http://www.cs.ox.ac.uk/files/3287/PRG05.pdf | ref=Scott(1976) }}
+* {{cite book| author=Henk Barendregt | url=http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf| chapter=Typed lambda calculi with types | title=Handbook of Logic in Computer Science| volume=Volume II | publisher=Oxford University Press | year=1992 }}
 {{DEFAULTSORT:かたつきらむたけいさん}}