（λx.xy）xの自由変数xおよびλxy.xのバウンド変数

Question

私はラムダ計算で演習を解決していました。しかし、私の解決策は答えとは異なり、何が間違っているのかわかりません。

1. $（ lambda x.xy）x $の自由変数を見つけます。
   私のワーキング：$ fv（（ lambda x.xy）x）= fv（ lambda x.xy） cup fv（x）= {y } cup {x } = {x、y } $。
   モデルの回答：$ fv（（ lambda x.xy）x）= {x } $。

2. $ lambda xy.x $のバウンド変数を見つけます。
   私の仕組み：可変$ y $にはバインディングがありますが、$ lambda $ -Abstractionの本文には存在しないため、拘束できないため、$ bv（ lambda xy.x）= {x } $それだけ。
   モデルの回答：$ bv（ lambda xy.x）= {x、y } $。

Answer 1

1. あなたの答えは正しいです、$ y $は確かに無料です。モデル1は間違っています。たぶんタイプミスがあり、答えは$（ lambda y.xy）x $を意味していました

2. $ bv $の正確な定義に依存します。多くの場合、$ fv $のみが正式に定義されます。これは、より重要であるためです。 （バインドされた変数は可能です 自由に名前が変更されました したがって、$ bv $が begin {eqnarray*} bv（x）＆=＆ {} bv（mn）＆=＆bv（m）として定義されている場合。 cup bv（n） bv（ lambda xm）＆=＆ {x } cup bv（m） end {eqnarray*}モデルの答えは正しいです。この定義は理にかなっていることに注意してください：用語$ m $があり、無料変数$ x $の別の用語$ n $をバインドされた変数なし（$ bv（n）= {} $） $ bv（m）= bv（m [x：= n]）$。 $ lambda $の下にも表示されるバインドされた変数のみを検討する場合、このプロパティは保持されません。