単純型付きラムダ計算
Syntax
code:BNF
A ::= a | A -> B
M ::= (x: A) | (lambda (x: A) M) | (M N)
型の決定
$ (x: A)
の型は
$ A
$ M
の型が
$ B
ならば，
$ (lambda (x: A) M)
は
$ A \rightarrow B
$ M
の型が
$ A \rightarrow B
かつ
$ N
の型が
$ A
ならば，
$ (M N)
は
$ B
See also:
ラムダ計算