原始帰納的関数としての if

問：以下の原始帰納的を構成せよ

sub:N×N→N　sub(x,y)=x-y if x ≧ y, otherwise 0;
max
less
mod
gcd

etc.etc... とかいう感じの課題が出ました。

いや、正直直接やることもできるんですが、原始帰納的関数 (PRF) として if B then X else Y が定義できちゃえば楽です。

というわけで、PRFとしての if( x, y, z )

if( x, y, z ) を定義したいんですが、ちょっと引数の順番がこのままでは都合が悪いので、if'( y, z, x) と変数の順序を変えたものを考えます。if は射影関数とif'との合成関数になるので、if' がPRFならば、ifもPRFです。以下正論理（0をFalse、1以上をTrueとみなす）の場合です

define if'( x_1, x_2, y )

case y = 0;
if'( x_1, x_2, 0 ) = P^2_2(  x_1, x_2 ) = x_2

otherwise
if'( x_1, x_2, y+1 ) = P^4_1( x_1, x_2, y, if( x_1, x_2, y ) ) = x_1

こうして if' を原始帰納的関数として定義することができました。射影関数を使ってやって、変数の順序を if'( x1, x2, y ) = if( y, x1, x2 ) となるように入れ替えると。

if( b, M, L ) は b の値に応じて M か L を返します。

あとは

例えば最大値を返す max( x, y ) なんかは、 　 max( x, y ) = if( sub( x, y ), x, y ) 簡単ですね。

これで勝つる。