原始帰納的関数の例
これらは全て原始帰納的関数
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 はsuccessorhss :: Int -> Int
s 0 = 1
s n = n+1 p はpredecessorhsp :: Int -> Int
p 0 = 0
p n = n-1初期関数で定義できる
hsp 0 = c0
p x+1 = u^2_1 x (pred x)加算関数plus
plusplus(0,y) = y
plus(x+1, y) = s(plus(x, y))hsplus :: Int -> Int -> Int
plus 0 y = y
plus x y = s $ plus (x-1) y本来は
- は使えないので、Haskellでの定義はちょっとせこい自然数上の減算関数sub
負数になはならず、最小値は0
ex. 9-10=0
subsub(x, 0) = x
sub(x, y+1) = p(sub(x,y))↑の
+ は本当は上で定義した関数plusを使うhssub :: Int -> Int -> Int
sub x 0 = x
sub x y = p $ sub x (y-1) - を定義しているので、Haskellでの定義の右辺で - があるのはおかしいが、無理なのでこうしてる思ったが、これIdrisならきれいに定義できるかも
乗算関数mult
multmult(0, y) = 0
mult(x+1, y) = mult(x,y) + yhsmult :: Int -> Int -> Int
mult 0 y = 0
mult x y = plus (mult (x-1) y) y除算関数quo
たくさんの補助関数が必要になる
div と rem はもともとHaskellにあるので再定義してるhssg 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を返す
論理式
否定と論理積があれば、論理和と含意を作れる
否定\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~