pi8027/typeinfer — Issue #46: 図1.7のT-ABSに関する疑問
Author: cutsea110
Created: 2011-11-13 23:18:51+00:00
State: open

図1.7の単純型付きλ計算の型判定のT-ABSに関して疑問。

Γにx:t1を加えた環境においてe:t2ならば、Γにおいてλx.eの型がt1->t2とあるんですが、
これってΓにx:t1を加えた環境においてλx.eの型がt1->t2となるんではないか？という気がしました。
つまり

Γ, x : t1 ⊢ e : t2
ーーーーーーーーー [T-Abs]
Γ ⊢ λx.e : t1 → t2

じゃなくて

Γ, x : t1 ⊢ e : t2
ーーーーーーーーー [T-Abs]
Γ,x:t1 ⊢ λx.e : t1 → t2
~~~~

なんじゃなかろうか？という疑問がでてきました。