Download presentation
Presentation is loading. Please wait.
1
型理論 ラッセルのパラドックス： 「集合の集合」は矛盾を引き起こす。 ラッセル、ホワイトヘッド 「プリンキピアマセマティカ」
プログラミング言語のコンパイル時チェック
2
型つきl計算 型 Type::= BaseType | Type → Type | Type ×Type
BaseType ::=a | b | … (基底型は型) l項 Var ::= v | Var ’ Term ::= Var | (Term Term) | (l Var:Type. Term) | < Term, Term> 略記法は型なしと同様
3
型判定 型判定式 型推論法則
4
breduction
5
構成的プログラミング 型を命題と考え, と解釈すれば(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
6
型つきl計算の性質 無限の長さのb簡約列は存在しない （強正規化可能） 計算が必ず止まる 不動点演算子が存在しない
7
GUIにあらわれる関数概念 例示によるプログラミング (Programming by Demonstration, PBD) 作業の再帰定義
(Rule-Based) Visual Languages
8
Dependency Tree Data Structure
9
Fixpoint Operator on Dependency Tree
10
Fixpoint figure and its semantics
＝ Fix/3: fixpoint figure of arity 3
Similar presentations
