プログラミング言語論（2023 年度）テスト解答例（一部）

1. (λ z w. z w w)(λ x y. x)(λ x y. y)
   ⇒ (λ w. (λ x y. x) w w)(λ x y. y)
   ⇒ (λ x y. x)(λ x y. y)(λ x y. y)
   ⇒ (λ z x y. y)(λ x y. y) （ただし z は任意のフレッシュな名前）
   ⇒ λ x y. y
   

2. (λ a b. b a) (λ f x. f x) (λ f x. f (f x))
   ⇒ (λ b. b (λ f x. f x)) (λ f x. f (f x))
   ⇒ (λ f x. f (f x)) (λ f x. f x)
   ⇒ λ x. (λ f x. f x)((λ f x. f x) x)
   ⇒ λ x y. (λ f x. f x) x y （ただし y は任意のフレッシュな名前）
   ⇒ λ x y. (λ z. x z) y （ただし z は任意のフレッシュな名前、ここで打ち切っても良い）
   ⇒ λ x y. x y
   

3. (λ m n f x. m f (n f x)) (λ f x. f (f x))(λ f x. f x)
   ⇒ (λ n f x. (λ f x. f (f x)) f (n f x)) (λ f x. f x)
   ⇒ λ f x. (λ f x. f (f x)) f ((λ f x. f x) f x)
   ⇒ λ f x. (λ x. f (f x)) ((λ f x. f x) f x)
   ⇒ λ f x. f (f ((λ f x. f x) f x))
   ⇒ λ f x. f (f ((λ x. f x) x)) （ここで打ち切っても良い）
   ⇒ λ f x. f (f (f x))