(*
*ペアノの公理による自然数の定義*0) 0 は自然数*1) x が自然数ならば s[x] ( =x+1) は自然数*2) 上記の規則でできる物だけが自然数である*)(*
*コード化 (数字列 0,1,2)、ペアノ形式 (0,s[0],s[s[0]]) 間の変換*ntop:N->P*pton:P->N*)ntop[0]:=0
ntop[x_]:=s[ntop[x-1]]

pton[0]:=0
pton[s[x_]]:=pton[x]+1

(*
*ペアノ形式での和*
*0+x=x*(x+1)+y=(x+y)+1*)

padd[0,x_]:=x
padd[s[x_],y_]:=s[padd[x,y]]

(*
*ペアノ形式での積*
*0*x=0*(x+1)*y=(x*y)+y*)

pmul[0,_]:=0
pmul[s[x_],y_]:=padd[pmul[x,y],y]

(*
*ペアノ形式での部分差 (x>y=>x-y,x<y=>0)*
*0-*-x=0*x-*-0=x*(x+1)-*-(y+1)=x-*-y*)

psub[0,_]:=0
psub[x_,0]:=x
psub[s[x_],s[y_]]:=psub[x,y]

(*
*ペアノ形式で整数を扱う*)

bar[pp[0,x_]]:=pp[0,x]
bar[pp[x_,0]]:=pp[x,0]
bar[pp[s[x_],s[y_]]]:=bar[pp[x,y]]

(*
*整数とそのペアノ形式の変換*)

ntoz[z_]:=pp[ntop[z],0]/;z≥0
ntoz[z_]:=pp[0,ntop[-z]]/;z<0

zton[pp[0,x_]]:=-pton[x]
zton[pp[x_,0]]:=pton[x]
zton[x_]:=zton[bar[x]]

(*
*if then else 関数*)

pifz[0,x_,_]:=x
pifz[_,_,y_]:=y

(*
*大小比較*)

pgt[x_,y_]:=pifz[psub[x,y],y,x]

plt[x_,y_]:=pifz[psub[x,y],x,y]

(*
*最大公約数*)

pgcm[0,x_]:=x
pgcm[x_,y_]:=pgcm[psub[pgt[x,y],plt[x,y]],plt[x,y]]

(*
*割り算*)

pdiv[0,_]:=0
pdiv[x_,y_]:=pifz[psub[s[x],y],0,s[pdiv[psub[x,y],y]]]

(*
*余り*)

prem[x_,y_]:=psub[x,pmul[y,pdiv[x,y]]]

(*
*符号の変更*)

zminus[pp[x_,y_]]:=pp[y,x]

(*
*絶対値*)

zabs[pp[0,x_]]:=pp[x,0]
zabs[z_]:=z

(*
*整数のペアノ形式*)

ztop[pp[x_,0]]:=x
ztop[pp[0,y_]]:=y

ptoz[x_]:=pp[x,0]

(*
*整数のペアノ形式での計算*)

zadd[pp[x_,y_],pp[u_,v_]]:=bar[pp[padd[x,u],padd[y,v]]]

zsub[x_,y_]:=zadd[x,zminus[y]]

zmul[pp[x_,y_],pp[u_,v_]]:=pp[padd[pmul[x,u],pmul[y,v]],padd[pmul[x,v],pmul[y,u]]]
zpmul[pp[x_,y_],z_]:=pp[pmul[x,z],pmul[y,z]]

zpdiv[pp[x_,y_],z_]:=pp[pdiv[x,z],pdiv[y,z]]

(*
*有理数のペアノ形式での計算*)

qbar[qq[x_,y_]]:=qq[zpdiv[x,pgcm[ztop[x],y]],pdiv[y,pgcm[ztop[x],y]]]

ntoq[{x_,y_}]:=qbar[qq[ntoz[x],ntop[y]]]
qton[qq[x_,y_]]:={zton[x],pton[y]}

qmul[qq[x_,y_],qq[u_,v_]]:=qbar[qq[zmul[x,u],pmul[y,v]]]

qadd[qq[x_,y_],qq[u_,v_]]:=qbar[qq[zadd[zpmul[x,v],zpmul[u,y]],pmul[y,v]]]

ntop[4]

padd[s[s[0]],s[s[s[0]]]]

pmul[s[s[0]],s[s[s[0]]]]

psub[ntop[5],ntop[3]]

psub[ntop[3],notp[5]]

ntop[5]

psub[ntop[3],ntop[5]]

bar[pp[ntop[5],ntop[3]]]

bar[pp[ntop[3],ntop[5]]]

ntoz[5]

ntoz[-5]

pgcm[ntop[12],ntop[18]]

pton[%101]

zadd[ntoz[3],ntoz[4]]

ntoq[{3,4}]

qton[ntoq[{12,8}]]

qadd[ntoq[{1,2}],ntoq[{1,3}]]

qton[%109]

(* qsub[qq[x_,y_],qq[u_,v_]]:= ... *)

qsub[ntoq[{1,2}],ntoq[{1,3}]]

qton[%]