(*
 * nat.txt (2012/11/27 版)
 *
 * ペアノの公理による自然数の定義
 *
 *	[ペアノの公理]
 *		0) 0 は自然数
 *		1) x が自然数ならば s[x] ( = x + 1 ) は自然数
 *		2) 上記の規則でできる物だけが自然数である
 *
 *	[注1] 高校までは、最小の自然数を 1 としてきた(0 を自然数に含めない)が、
 *		「数学」では「自然数に 0 を含めた方が色々と『便利』」なので
 *		大学では、「『0 を自然数に含める』事が多い」
 *
 *	[注2] ペアノの公理の 0) と 1) が帰納法の基礎になるが 2) も必要
 *		この 2) がないと、「全ての自然数について」と言う事ができなくなってしまう
 *			もし、0), 1) の規則では作れない自然数があったら、
 *			それは帰納法で扱う対象以外になってしまい、
 *			それについて何も言えないから..
 *)

(*
 * コード化 ( 自然数 0, 1, 2, .. ) と、ペアノ形式 ( 0, s[0], s[s[0]], .. ) 間の変換
 *	ntop : N -> P	// 自然数(N)からペアノ形式(P)への変換 (同型変換)
 *	pton : P -> N	// ペアノ形式(P)から自然数(N)への変換 (同型変換の逆変換)
 *
 *	[規則]
 *		ntop[0]		=	0
 *		ntop[n + 1]	=	s[ntop[n]]
 *
 *		pton[0]		=	0
 *		pton[s[p]]	=	pton[p] + 1
 *
 *	[説明]
 *		ntop は、N から P への同型対応(全単射)
 *			「同型」とするために、関数の対応も行う
 *		pton は、P から N への同型対応で、ntop の逆関数 ( ntop は pton の逆関数 )
 *)

ntop[0] := 0
ntop[x_] := s[ntop[x - 1]]

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

(*
 * 可換対応 ( pnApply )
 *	P の世界の関数 Fkp が N の世界のどのような関数 Fkn になるかを確認する
 *
 *	[規則]
 *		F1n[x]		=	pton[F1p[ntop[x]]]
 *		F2n[x,y]	=	pton[F2p[ntop[x],ntop[y]]]
 *
 *		pnApply[F1p,x]	=	F1n[x]
 *		pnApply[F2p,x,y]	=	F2n[x,y]
 *
 *	[説明]
 *		F1n(F2n) は N 上の 1(2) 変数関数
 *		F1p(F2p) は P 上の 1(2) 変数関数で、F1n(F2n) に対応する関数
 *			F1n(F2n) は、F1p(F2p) と、pton に関して「可換」
 *)

pnApply[f1p_,x_]		:=	pton[f1p[ntop[x]]]
pnApply[f2p_,x_,y_]	:=	pton[f2p[ntop[x],ntop[y]]]

(*
 * ペアノ形式での和 (padd)
 *
 *	[規則]
 *		    0     + x =       x
 *		( x + 1 ) + y = ( x + y ) + 1
 *
 *	[説明]
 *		padd[x,y] は P の世界の和の計算(足し算)
 *			pnApply[padd,x,y] = x + y
 *)

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

(*
 * ペアノ形式での積 (pmul)
 *
 *	[規則]
 *		    0     * x =       0
 *		( x + 1 ) * y = ( x * y ) + y
 *
 *	[説明]
 *		pmul[x,y] は P の世界の積の計算(かけ算)
 *			pnApply[pmul,x,y] = x * 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[x,y] は P の世界の部分差(引き算)
 *			ただし、負の数は配慮していないので、x >= y の時だけ差になる
 *			pnApply[psub,x,y] = x - y ( x >= y の時 )
 *			pnApply[psub,x,y] =   0   ( x < y の時 )
 *)

psub[0, _] := 0						(* 「_」のみで名前無しの変数を表す *)
psub[x_, 0] := x
psub[s[x_], s[y_]] := psub[x, y]

(*
 * ペアノ形式で整数を扱う
 *	整数 (Z) の要素とペアノ数の対応関係
 *		n : 1 以上の自然数
 *		p : n に対応するペアノ数
 *
 *		負の数
 *			z = - n		⇔		pp[0,p]
 *		零
 *			z =   0		⇔		pp[0,0]
 *		正の数
 *			z =   n		⇔		pp[p,0]
 *
 *		pp[p,q] と、「二つの自然数の対」で「整数」を表現できる.. ( が.. )
 *
 *	[ポイント]
 *		二つのペアノ数の対の集合
 *			PP = { pp[p,q] | p, q \in P }
 *		で、
 *			pp[p,q] ( p も q も 0 でない )
 *		は何を表すか ? を考える。
 *		直感的には、
 *			pp[p,q] は「p - q」に対応するので..
 *		PP に、同値関係
 *				pp[s[p],s[q]] 〜 pp[p,q]
 *		を導入し、
 *			Z = PP/〜
 *		とする。
 *
 *		すなわち、Z は PP を 〜で割った同値類の集合として定義する
 *
 *		bar[pp[p,q]] は、
 *			pp[p,q]と同値な代表元 pp[u,v]
 *		で、
 *			u,v の両方、あるいはどちらか一方が 0
 *		となるもの。
 *)

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

(*
 * 整数(Z)と自然数対(PP)との対応
 *
 *	ztopp : Z -> PP	// 整数(Z)からペアノ形式(PP)への変換 (同型変換)
 *	pptoz : PP -> Z // 逆変換
 *
 *)

ztopp[z_] := pp[ntop[z], 0] /; z >= 0
ztopp[z_] := pp[0, ntop[-z]] /; z < 0

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

(*
 * 可換対応 ( ppzApply )
 *	PP の世界の関数 Fkpp が Z の世界のどのような関数 Fkz になるかを確認する
 *
 *	[規則]
 *		F1z[x]		=	pptoz[F1pp[ztopp[x]]]
 *		F2z[x,y]	=	pptoz[F2pp[ztopp[x],ztopp[y]]]
 *
 *		ppzApply[F1pp,x]		=	F1z[x]
 *		ppzApply[F2pp,x,y]	=	F2z[x,y]
 *
 *	[説明]
 *		F1z(F2z) は Z 上の 1(2) 変数関数
 *		F1pp(F2pp) は PP 上の 1(2) 変数関数で、F1z(F2z) に対応する関数
 *			F1z(F2z) は、F1pp(F2pp) と、pptoz に関して「可換」
 *)

ppzApply[f1pp_,x_]		:=	pptoz[f1pp[ztopp[x]]]
ppzApply[f2pp_,x_,y_]	:=	pptoz[f2pp[ztopp[x],ztopp[y]]]

(*
 * if then else 関数
 *
 *	[説明]
 *								y		( x = 0 の時 )
 *		pifz[x,y,z] = {
 *								z		( それ以外の時 )
 *)

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

(*
 * 大小比較 ( max/min )
 *
 *	[説明]
 *		pgt[x,y] は x と y の小くない方 (max)
 *
 *								x		( x >= y の時 )
 *		pgt[x,y] = {
 *								y		( それ以外の時 )
 *
 *		plt[x,y] は x と y の大きくない方 (min)
 *
 *								x		( x <= y の時 )
 *		plt[x,y] = {
 *								y		( それ以外の時 )
 *
 *)

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

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

(*
 * 最大公約数
 *
 *	[規則] (ユークリッドの互除法)
 *		gcm(0,x) = x			// 0 と x の gcm は x
 *		gcm(x,y) = gcm(x-y,y)	// x >= y の時
 *		gcm(x,y) = gcm(y-x,x)	// x < y の時
 *
 *	[説明]
 *		pgcm[x,y] は x と y の最大公約数
 *)

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

(*
 * 整数割り算 (pdiv)
 *
 *	[規則]
 *		0 / x = 0
 *		x / y = ( ( x - y ) / y ) + 1		( x >= y の時 )
 *		x / y = 0							( x < y の時 )
 *
 *	[説明]
 *		pdiv(x,y) は、x を y で割った商を求める関数
 *)

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

(*
 * 余り (prem)
 *
 *	[規則]
 *		x mod y = x - ( x / y ) * y
 *
 *	[説明]
 *		prem(x,y) は、x を y で割った余りを計算する
 *)

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

(*
 * 符号の変更 (zminus)
 *
 *	[規則]
 *		- pp[x,y] = pp[y,x]
 *
 *	[説明]
 *		zminus は符号を変換する
 *)

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

(*
 * 絶対値 (zabs)
 *
 *	[規則]
 *		|n|	=	n	( n >= 0 )
 *		|n|	=	-n	( n < 0 )
 *
 *	[説明]
 *		zabs は絶対値を求める
 *)

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

(*
 * 整数の絶対値をペアノ形式にする
 *
 *	[規則]
 *		pp[u,0] = u
 *		pp[0,v] = v
 *
 *	[説明]
 *		ztoap は PP 形式の整数の絶対値をペアノの形式の自然数にする
 *)

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

(*
 * 整数のペアノ形式での計算
 *
 *	[説明]
 *		zadd は PP 形式の整数同士の足し算
 *			ppzApply[zadd,u,v] = u + v
 *		zsub は PP 形式の整数同士の引き算
 *			ppzApply[zsub,u,v] = u - v
 *		zmul は PP 形式の整数同士のかけ算
 *			ppzApply[zmul,u,v] = u * v
 *		zpmul は PP 形式の整数に P 形式の自然数を掛けたもの
 *		zpdiv は PP 形式の整数を P 形式の自然数で割ったもの
 *)

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]]

(*
 * ペアノ形式で有理数を扱う
 *	有理数 (Q) の要素とペアノ数の対応関係
 *		d : 整数
 *		q : 0 より大きな自然数
 *
 *		u : d に対応する PP 形式の整数
 *		v : q に対応する P 形式の自然数
 *
 *		分数
 *			d/u			⇔		zp[u,v]
 *
 *		zp[u,v] と、「整数と自然数の対」で「有理数」を表現できる.. ( が.. )
 *
 *	[ポイント]
 *		整数と自然数の対の集合
 *			ZP = { zp[d,q] | d \in PP, q \in P }
 *		で、
 *			gcm[d,q] > 1
 *		は何を表すか ? を考える。
 *		直感的には、
 *			zp[d,q] は「d/q」に対応するので..
 *		ZP に、同値関係
 *				zp[d,q] 〜 zp[g*d,g*q]	( g は 1 より大きい自然数 )
 *		を導入し、
 *			Q = ZP/〜
 *		とする。
 *
 *		すなわち、Q は ZP を 〜で割った同値類の集合として定義する
 *
 *		qbar[zp[d,q]] は、
 *			zp[d,q]と同値な代表元 zp[u,v]
 *		で、
 *			u,v は互に素
 *		となるもの。
 *
 *	[説明]
 *		qbar : ZP 形式の代表元を求める
 *		qtozp : 整数の対(有理数)を ZP 形式にする
 *		zptoq : ZP 形式を整数の対(有理数)に直す
 *)

qbar[zp[x_,y_]] := zp[zpdiv[x,pgcm[ztoap[x],y]],pdiv[y,pgcm[ztoap[x],y]]]

qtozp[{x_,y_}] := qbar[zp[ztopp[x],ntop[y]]]
zptoq[zp[x_,y_]] := {pptoz[x],pton[y]}

(*
 * 可換対応 ( qzpApply )
 *	ZP の世界の関数 Fkzp が Q の世界のどのような関数 Fkq になるかを確認する
 *
 *	[規則]
 *		F1q[x]		=	zptoq[F1zp[qtozp[x]]]
 *		F2n[x,y]	=	zptoq[F2zp[qtozp[x],qtozp[y]]]
 *
 *		qzpApply[F1zq,x]	=	F1q[x]
 *		qzpApply[F2zq,x,y]	=	F2q[x,y]
 *
 *	[説明]
 *		F1q(F2q) は Q 上の 1(2) 変数関数
 *		F1zp(F2zp) は ZP 上の 1(2) 変数関数で、F1q(F2q) に対応する関数
 *			F1q(F2q) は、F1zp(F2zp) と、qtozp に関して「可換」
 *)

qzpApply[f1zp_,x_]		:=	zptoq[f1zp[qtozp[x]]]
qzpApply[f2zp_,x_,y_]	:=	zptoq[f2zp[qtozp[x],qtozp[y]]]

(*
 * 有理数のペアノ形式での計算
 *
 *	[説明]
 *		qmul : ZP 形式のかけ算
 *			qzpApply(qmul,u,v) = u * v
 *		qadd : ZP 形式の足し算
 *			qzpApply(qdiv,u,v) = u / v
 *)

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

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

(*
 * 課題
 *
 * 有理数のペアノ形式での引き算 (qsub)
 *
 *	[規則]
 *		(x/y) - (z/w) = (x/y) + ((-z)/w)
 *
 *	[説明]
 *		qsub : ZP 形式の引き算
 *			qzpApply(qsub,u,v) = u - v
 *
 *)