機能からCL項を逆算するための初等的方法

機能から CL 項を逆算するための初等的方法
大島理総 ∗
†
平成 27 年 2 月 22 日
組み合わせ論理における CL 項は引数をとる関数を表していると解釈でき
る．CL 項が与えられれば機械的な操作によって値を計算できるが，逆に，関
数としての機能が与えられたとき，それを実現する CL 項を求めるにはどう
すればよいだろうか．この点を例題に即して考えてみる．
例題 1 M xyz ▷ xy となるような M を求めよ．
解答 M が M0 a という形をしているものとする．試みに M0 ≡ B として計算
してみると Baxyz ▷ a(xy)z となるので a として K を採用すれば目的は達せ
られる．
例題 2 M xy ▷ yx となるような M を求めよ．
解答はじめから BM0 N0 xy ▷ yx となるような M0 ，N0 だけを考えることに
する．このとき，BM0 N0 xy ▷ M0 (N0 x)y であるが，もし，M0 が SM1 と書
けたとすると SM1 (N0 x)y ▷ M1 y(N0 xy)．そこで，M1 として I，N0 として
K を採用すれば目的は達せられる．すなわち，M として B(SI)K を採用すれ
ばよい．
このように，解答の各ステップ毎でどのような形の項を想定するかは（い
まのところ）直観と経験に依存する．しかしながら，組み合わせ論理につい
ての一般論を勉強すれば，欲しい機能を CL 項として実現するための有力な
道具が得られるに違いない．
∗ 学習院大学理学部数学科
† 目白ロジックサークル
1

Download Report