% $Id: Unary.oz,v 1.2 2008/12/05 04:50:40 leavens Exp leavens $ % Natural numbers in unary notation % % Grammar % ::= z "zero" % | s() "successor" declare % succeeds with each natural number (in order) proc {Count ?I} choice I = z [] I = s({Count}) end end % succeeds if X is strictly less than Y proc {LT ?X ?Y} choice local N in X=z Y=s(N) end [] local N M in X=s(N) Y=s(M) {LT N M} end end end % succeeds if N is X + Y proc {Plus ?X ?Y ?N} choice X=z Y=N [] M MPlusY in X=s(M) {Plus M Y MPlusY} N=s(MPlusY) end end % succeeds if N is X - Y proc {Minus ?X ?Y ?N} {Plus X N Y} end % succeeds if N is X times Y proc {Times ?X ?Y ?N} choice X=z N=z [] X=s(z) N=Y [] local M K KTimesY in X=s(s(M)) % make this case disjoint % from the previous case K=s(M) % but we don't want to induct on M... {Times K Y KTimesY} {Plus Y KTimesY N} end end end % succeeds if I is the integer corresponding to N proc {ToInt N ?I} choice N=z I=0 [] M J in N=s(M) {ToInt M J} I=J+1 end end % succeeds if N is the natural nubmer corresponding to I proc {ToNat I ?N} choice I=0 N=z [] M J in (I>0)=true J=I-1 {ToNat J M} N=s(M) end end