pi8027/typeinfer — Issue #36: 1.3 α同値の「項eに自由出現する変数xを」は自由出現でいい？
Author: cutsea110
Created: 2011-11-13 22:52:15+00:00
State: open

P5の3行目、「項eに自由出現する変数x」を全て置き換えるとあるけど、これは自由出現でいいの？

「この関係を定義するためには、置き換える対象の束縛変数を束縛しているλ抽象λx.eに関して自由出現する変数xを置き換えて項を考える必要があります」
という文章はその直前の「例えばλx.xはλy.yとα同値です。」を受けての説明だとすれば自由変数でなく束縛変数を置き換えたものって気がしました。

なんか私が勘違いしているかもしれないけど。