目次

引用

導出

参考資料

引用する

王垠は博文「GTF-Great Teacher Friedman」で、コネル大学の同級生が1週間かけて前駆関数を考え出したチャーチ符号化について、クリンニの最初の設計とは全く異なると述べた.
ウィキペディアのチャーチコードのフレーズには、この2つの方法が紹介されています.
ゆえにλ演算は「無状態」であり,前駆関数を構築するのは確かに簡単ではない.
1つの方法(クリンニが最初に構築したものかもしれない)は、まず秩序対を構築し、秩序対によって2つの隣接する数を保存することによって、前駆関数を実現する.この方法は理解しやすく、チャーチ符号化を話す多くの本が話せる方法でもある.
王垠のこの同級生が考えている方法は分かりにくい.概念的には,丘奇数を特殊な構造Valueにカプセル化し,丘奇数に対するシフトを実現した後,(Value→Value)型の後継関数を再構築することである.公理「ある数の後が自然数0に対応するValue」により,「-1」のValue表現を構築し,前駆関数の構築に成功した.

ガイド人

以下では、パラメータとして1つの丘奇数を受け入れ、パラメータの前駆丘奇数を返す前駆関数をPREDと統一して記す.PREDの概略フレームワークは

(define PRED
  (lambda (number)
    (lambda (f x)
      ...)))

なお、(PRED ZERO)の値は、依然として奇数丘0 ZEROである.
秩序を立てて前駆関数を構築する方法は余計なことではありませんが、ここではウィキペディアで与えられた構造構想、つまり王垠が言った彼の同級生が与えた方法について具体的に話します.
まずは丘奇数の構造を振り返ってみます.丘奇数の構造構想は,関数ネスト層数で自然数を表現することである.この考え方によれば、丘奇数は、2つのパラメータを受け入れる.1つは、ネスト呼び出しを繰り返すための関数fであり、2つは、この関数に伝達されるパラメータxである.

(define ZERO
  (lambda (f x) x))
(define ONE
  (lambda (f x) (f x)))
(define TWO
  (lambda (f x) (f (f x))))

後続関数SUCCは、既存の丘奇数に基づいてfを1層多くネストし、新しい丘奇数に戻ると容易に構築できる.

(define SUCC
  (lambda (number)
    (lambda (f x)
      (f (number f x)))))

複数のネストは簡単ですが、1つのネストを外すのは面倒です.PREDを構築する鍵は、「再定義」キュー奇数および後続関数にある.パッケージ化の手段により、VALUEと記載された丘奇数の容器を構築することができる.これは、入力されたキュー奇数をパラメータの位置に保存する閉パケット(の戻り値、すなわちネストされた呼び出し部(f..(f x)..)、簡潔化のため、以下同様)を受け入れ、

(define VALUE
  (lambda (number)
    (lambda (package)
      (package number))))

わかりやすく、

((VALUE n) f) = (f n)  （ (*)）

この性質を利用して、パッケージ化されたVALUEからEXTRACTを得るための補助関数numberを構築することができる.

(define EXTRACT
  (lambda (value)
    (value (lambda (x) x))))

上の性質は後続関数の挙動に非常に近い.この性質に基づいて、新しい後継関数INCを構築することができ、丘奇数後継関数とは異なり、INCはパッケージ化されたVALUEを入力とし、その後のVALUEを出力とする.

;; VALUE -> VALUE
(define INC
  (lambda (value)
    (lambda (package)
      (package (value f)))))

(value f)は元の丘奇数の後継数(丘奇数でもある)を得るため、INCはそれをVALUEに再カプセル化する必要がある.なお、INCは自由変数fを導入しているが、このfはPREDのフレームワーク(すなわち、丘奇数に必要なf)にすでに現れているので、実際には制約されている.
次のステップでは、INCの繰返し特性を検証し、"-1"に対応するVALUEを構築し、これを反復開始点とする.
表記V0 = (VALUE x)は、性質(*)およびINCによって定義される.

            V0 = (VALUE x)
      (INC V0) = (VALUE (f x)) = V1
(INC (INC V0)) = (VALUE (f (f x))) = V2
              ...
      (INC Vn) = V[n+1]

INCをV0でn回繰り返し呼び出すと(nは丘奇数)、

(n INC V0) = Vn

ここでVnは、自然数nに対応するVALUEとして理解される.前駆関数を構築するには、V[-1]ではなくV[-1]からこの反復プロセスを開始する「−1」、すなわちV0を再構築するだけで、前駆関数を実現することができる.
明らかに、V[-1]は性質を有しなければならない.

(INC V[-1]) = (VALUE x) = V0

展開

(lambda (package) (package (V[-1] f))) = (lambda (package) (package x))

これにより得られる(合一)、

(V[-1] f) = x

適用η-変換可能

V[-1] = (lambda (u) x)

V[-1]およびV0を観察すると、V[-1]は実際には丘奇数の0に対応し、V0は丘奇数の1に対応することが分かった.つまり、**はVALUEのカプセル化により、丘奇数を"左シフト"する目的を達成し、丘奇数の"-1"から反復させ、丘奇数で結果を返し、前駆の効果を実現する.**次のようになります.

(n INC V[-1]) = V[n-1]

得られたVALUEに対応するキュー奇数ネスト形式をEXTRACTを用いて抽出し,PRED関数の関数体を得た.なお、(EXTRACT V[-1]) = xであるため、(PRED ZERO) = ZEROは満足である.
最後に、前の構成のVALUE(補助関数、実際には必要ありません)、EXTRACT、INCを組み合わせて、PRED関数を得ることができます.

(define TEN
  (lambda (f x) (f (f (f (f (f (f (f (f (f (f x))))))))))))

(define PRED
  (lambda (number)
    (lambda (f x)
      (define EXTRACT
        (lambda (value)
          (value (lambda (x) x))))
      (define INC
        (lambda (value)
          (lambda (package)
            (package (value f)))))
      (define V-1
        (lambda (u) x))
      (EXTRACT (number INC V-1)))))

((PRED TEN)
 (lambda (x) (+ x 1))
 0)

以下に簡略化:

(define PRED
  (lambda (number)
    (lambda (f x)
      ((number
        (lambda (value)
          (lambda (package)
            (package (value f))))
        (lambda (u) x))
       (lambda (x) x)))))

これが最終的に得られた前駆関数である.

参考資料

王垠GTF - Great Teacher Friedman

ウィキペディア:チャーチコード