型理論 ラッセルのパラドックス： 「集合の集合」は矛盾を引き起こす。 ラッセル、ホワイトヘッド 「プリンキピアマセマティカ」 プログラミング言語のコンパイル時チェック
型つきl計算 型 Type::= BaseType | Type → Type | Type ×Type BaseType ::=a | b | … (基底型は型) l項 Var ::= v | Var ’ Term ::= Var | (Term Term) | (l Var:Type. Term) | < Term, Term> 略記法は型なしと同様
型判定 型判定式 型推論法則
breduction
構成的プログラミング 型を命題と考え, と解釈すれば(Curry-Howard Isomorphism) 、 型つきλ項は述語論理の証明。 自動証明器にかければ自動的にプログラムができる？ Martin-Lof, P. : Constructive mathematics and computer programming, in Logic, Methodology, and Philosophy of Science IV, Cohen, L. J. et al. eds., North-Holland(1982), pp.153-179.
型つきl計算の性質 無限の長さのb簡約列は存在しない （強正規化可能） 計算が必ず止まる 不動点演算子が存在しない
GUIにあらわれる関数概念 例示によるプログラミング (Programming by Demonstration, PBD) 作業の再帰定義 (Rule-Based) Visual Languages
Dependency Tree Data Structure
Fixpoint Operator on Dependency Tree
Fixpoint figure and its semantics ＝ Fix/3: fixpoint figure of arity 3