原始帰納的関数の例

チャーチ数と同じ考え方だが、自然数を扱える分こちらのほうが理解しやすい

これらは全て原始帰納的関数

k変数定数関数

定数関数0

$ f(\vec{x})=\mathrm{zero}()

定数関数c

zeroとsのc回組み合わせ

例えば$ c=3の場合

$ f(\vec{x})=s(s(s(\mathrm{zero}())))=0

ちゃんと書くには$ f_1=s(z),f_2=s(f_1),f_3=s(f_2)と書かないといけない

sはsuccessor

code:hs

s :: Int -> Int

s 0 = 1

s n = n+1

pはpredecessor

code:hs

p :: Int -> Int

p 0 = 0

p n = n-1

初期関数で定義できる

code:hs

p 0 = c0

p x+1 = u^2_1 x (pred x)

加算関数plus

code:plus

plus(0,y) = y

plus(x+1, y) = s(plus(x, y))

code:hs

plus :: Int -> Int -> Int

plus 0 y = y

plus x y = s $ plus (x-1) y

本来は-は使えないので、Haskellでの定義はちょっとせこいmrsekut.icon

自然数上の減算関数sub

負数になはならず、最小値は0

ex. 9-10=0

code:sub

sub(x, 0) = x

sub(x, y+1) = p(sub(x,y))

↑の+は本当は上で定義した関数plusを使う

code:hs

sub :: Int -> Int -> Int

sub x 0 = x

sub x y = p $ sub x (y-1)

-を定義しているので、Haskellでの定義の右辺で-があるのはおかしいが、無理なのでこうしてる

思ったが、これIdrisならきれいに定義できるかもmrsekut.icon

乗算関数mult

code:mult

mult(0, y) = 0

mult(x+1, y) = mult(x,y) + y

code:hs

mult :: Int -> Int -> Int

mult 0 y = 0

mult x y = plus (mult (x-1) y) y

除算関数quo

『(理論)12 計算モデルの基礎理論』.icon p46-

たくさんの補助関数が必要になる

divとremはもともとHaskellにあるので再定義してる

code:hs

sg x

| x == 0 = 0

| otherwise = 1 -- 本当はx>0のとき(x<0のときは未定義)

-- sgの逆

sg' x

| x == 0 = 1

| otherwise = 0 -- 本当はx>0のとき(x<0のときは未定義)

-- 剰余を計算

rem' 0 y = 0

rem' x y

| (1 + rem' (x-1) y) < y = 1 + rem' (x-1) y

| otherwise = 0

div' x y = sg' $ rem' x y

quo :: Int -> Int -> Int

quo 0 y = 0

quo x y = (quo (x-1) y) + (sg (div' x y))

isZero

isZero(x) := sub(1-x)

$ x=0のときのみ1を返す

論理式

以下では述語$ A,Bの定義関数をそれぞれ$ f_A,f_Bとする

否定と論理積があれば、論理和と含意を作れる

否定$ \lnot

$ f_{\lnot A}(\vec{x})=1-f_A(\vec{x})　

sub(1, fA(x))

論理積$ \land

$ f_{A\land B}(\vec{x})=f_A(\vec{x})\times f_B(\vec{x})

mult(fA(x), fB(x))

論理和$ \lor

$ A\lor B = \lnot(\lnot A\land \lnot B)なので、

$ f_{A\lor B}(\vec{x})=1-((1-f_A(\vec{x}))\times(1-f_B(\vec{x})))

含意$ \Rightarrow

$ A\Rightarrow B = \lnot(A\land\lnot B)なので、

$ f_{A\Rightarrow B }=1-(f_A(\vec{x})\times(1-f_B(\vec{x})))

2変数述語

$ x\le y := \mathrm{isZero}(x-y)

isZero(sub(x,y))

$ x=y := (x\le y)\land(y\le x)

$ x\lt y := s(x)\le y

isZero(sub(s(x),y))

量化

$ (\exists u<y) P(\vec{x}, u)となる論理式$ Q(\vec{x},y)

この式を$ \exists u \in \mathbb{N}(u<y) \wedge P(\vec{x}, u)] と変換して

$ Q(\vec{x}, y) :=(\mu z<y[P(\vec{x}, z)])<y

$ \muは有界最小化のもの

$ (\forall u<y) P(\vec{x}, u)となる論理式$ R(\vec{x},y)

この式を$ \forall u \in \mathbb{N}[(u<y) \Rightarrow P(\vec{x}, u)] と変換して

$ R(\vec{x}, y):=\neg(\exists u<y)[\neg P(\vec{x}, u)]

$ \left(\forall u_{(y \leq u \leq z)}\right) P(\vec{x}, u)となる論理式$ S(\vec{x},y,z)

この式を$ \forall u \in \mathbb{N}[(y \leq u \leq z) \Rightarrow P(\vec{x}, u)] と変換して

$ S(\vec{x}, y, z):=\forall u<(z+1)[(u<y) \vee P(\vec{x}, u)]

参考

『(理論)12 計算モデルの基礎理論』 3.6章

『C言語による計算の理論』 p.72~