lambda-calculus - 関数のラムダ計算削減

Question

私はラムダ計算が初めてで、チュートリアルを読んでいるときにこれに出くわしました。これが私の方程式です。

Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx))

ここで、別の項、たとえば F (YF) を適用すると、これをどのように減らすことができますか? ベータ簡約に従って私が正しければ、 ( ƛx.f(xx))のすべてのfを ( ƛx. f(xx))、これは正しいですか。そうであれば、どうすればそれを行うことができますか。

ありがとう

Answer 1

再生手順:

Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx)) = ƛf.( f ( ƛx.f(xx) ƛx.f(xx) ) ) 
  = ƛf.( f ( f (ƛx.f(xx) ƛx.f(xx)))) 
  = ƛf.( f ( f ( f (ƛx.f(xx) ƛx.f(xx)))) 
  = ƛf.( f ( f ( f ( f (ƛx.f(xx) ƛx.f(xx))))) = ...

したがって、このラムダ項は無限ループに入ります...

説明:置換する用語を見
てみましょう。これは=> 用語自体を活性化することを意味します。 次のように見る方が簡単かもしれません:を有効にして入力を提供すると (これは で置き換えられます)、結果は次のようになります: 同じプロセスを何度も繰り返すことができ、ラムダ式は消費されるだけです。 ..( ƛx.f(xx) ƛx.f(xx) )ƛx.f(xx)f'
(f' f')f'

( ƛy.f(yy) ƛx.f(xx) )ƛy.f(yy)yƛx.f(xx)f(ƛx.f(xx) ƛx.f(xx))

注意:
書くのは間違っています:
Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx)) 実際にはこうあるべきです: と Y = ƛf.(ƛx.f(xx) ƛx.f(xx))
の違いは、ƛx.f(xx)と(ƛx.f(xx))のアクティベーションであることです。アクティベートするには(入力)が必要なので、ƛx.f(xx)このようにアクティベートしても意味がありません。最後に:意味:(ƛx.f(xx))x


Y = ƛf.( ƛx.f(xx)) ( ƛx.f(xx)) = ƛf.( f ( ƛx.f(xx) ƛx.f(xx) ) )

YF = ( ƛx.F(xx)) ( ƛx.F(xx)) = F(ƛx.F(xx)) ( ƛx.F(xx)) = F(YF)