<> a <http://www.w3.org/2000/10/swap/log#N3Document>.

@prefix dc: <http://purl.org/dc/elements/1.1/>.
@prefix ed: <http://www.w3.org/2000/08/eb58#>.

<> dc:description """Primitive Recursive Arithmetic;
a foundational system, suggested in the QED project.
$Id: pra.n3,v 1.2 2002/01/24 21:33:16 connolly Exp $""";
  dc:source [
    = <http://www.earlham.edu/~peters/courses/logsys/recursiv.htm>;
    dc:title "Peter Suber, Recursive Function Theory";
  ];
  dc:source <http://ilrt.org/discovery/chatlogs/rdfig/2002-01-11#T19-52-39>;
  dc:source [ = <http://theory.stanford.edu/people/uribe/mail/qed.messages/22.html>;
    ed:excerpt """
I should temper my gospel fervor enthusiasm for PRA by observing that
while I agree with Tait (Finitism, J. of Philosophy, 1981, 78,
524-546) that PRA is THE NECESSARY AND SUFFICIENT logic for talking
about logics and proofs, there exists at least someone who refuses to
believe in PRA (Yessenin-Volpin, The Ultra-Intuitionistic Criticism
..., Intuitionism and Proof Theory, North-Holland, 1970, pp. 3-45).
But this fellow also refuses to believe in 10^12, which seems to fly
in the face of teraflops and terabyte memories."""]
.


@prefix r: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix s: <http://www.w3.org/2000/01/rdf-schema#>.

@prefix log: <http://www.w3.org/2000/10/swap/log#>.


@prefix : <pra#>.
@prefix pra: <pra#>.

this log:forAll
  :x, :y, :z,
  :f, :g, :h,
  :x0,
  :sy, :xsy, :hxsy, :xy, :hxy, :xhxy, :gxhxy.


:Natural a s:Class; s:label "Natural numbers".

:Natural is r:type of "0".

:PrimitiveRecursiveFunction a s:Class; s:label "Primitive Recursive Function";
  s:subClassOf r:Property.

:IntialFunction s:label "Inital Function";
  s:subClassOf :PrimitiveRecursiveFunction.

:z a :InitialFunction; s:label "z";
  s:domain :Natural;
  s:range :Natural;
  s:comment "z(x) = 0".

{ :x a :Natural } log:implies { :x :z "0" }.

:s a :IntialFunction; s:label "s";
  s:domain :Natural;
  s:range :Natural;
  s:comment """s(x) = successor of x (roughly, "x + 1")""".

:id a :InitialFunction; s:label "id";
  s:domain :Natural;
  s:range :Natural;
  s:comment "id(x) = x".

{ :x a :Natural } log:implies { :x :id :x }.

:id21 a :InitialFunction; s:label "id2,1";
  s:domain :PairOfNatural;
  s:range :Natural;
  s:comment "id2,1(x,y) = x".

:id22 a :InitialFunction; s:label "id2,2";
  s:domain :PairOfNatural;
  s:range :Natural;
  s:comment "id2,1(x,y) = y".


# axiom of pairs...
{ :x a :Natural.
  :y a :Natural. }
  log:implies { [ :id21 :x; :id22 :y ] }.


:composes a r:Property; s:label "composes";
  s:domain :PrimitiveRecursiveFunction;
  s:range  :PrimitiveRecursiveFunction;
  s:seeAlso :with.

:with a r:Property; s:label "with";
  s:domain :PrimitiveRecursiveFunction;
  s:range  :PrimitiveRecursiveFunction;
  s:comment """s(z(x)) = 1
s(s(z(x))) = 2 and so on. """.

{ :h :composes :f; :with :g.
  :y a :Natural.
  :z a :Natural.

  :x :g :y.
  :y :f :z.
}
  log:implies { :x :h :z }.


:case0 a r:Property; s:label "case 0";
  s:domain :PrimitiveRecursiveFunction;
  s:range  :PrimitiveRecursiveFunction;
  s:seeAlso :caseS.

:caseS a r:Property; s:label "case s(x)";
  s:comment """ Function h is defined through functions f and g by primitive recursion when
h(x,0) = f(x)
h(x,s(y)) = g(x,h(x,y)) """.

{ :h :case0 :f.
  :x a :Natural.
  :y a :Natural.

  :x0 :id21 :x; :id22 "0".
  :x :f :y.
}
  log:implies { :x0 :h :y }.


{ :h :caseS :g.
  :x a :Natural.
  :y :s :sy.

  :xsy :id21 :x; :id22 :sy.
  :xy :id21 :x; :id22 :y.
  :xhxy :id21 :x; :id22 :hxy.

  :hxy is :h of :xy.

  :gxhxy is :g of :xhxy.

}
  log:implies { :gxhxy is :h of :xsy.  }.


### test: can we define plus?

:plusAux :composes :s; :with :id22.

:plus :case0 :id; :caseS :plusAux.

"0" :s "1".
"1" :s "2".
"2" :s "3".
"3" :s "4".
"4" :s "5".

##### a little bit of RDFS
{ :x [ s:subPropertyOf :z ] :y } log:implies { :x :z :y }.
{ :x [ s:range :z ] :y } log:implies { :y a :z }.
{ :x [ s:domain :z ] :y } log:implies { :x a :z }.
{ :x a [ s:subClassOf :y ] } log:implies { :x a :y }.

s:subClassOf s:domain s:Class; s:range s:Class.
s:domain s:domain r:Property; s:range s:Class.
s:range s:domain r:Property; s:range s:Class.


#@@ bounded minimization

:minimizes s:label "minimizes";
  s:domain :PrimitiveRecursiveFunction;
  s:range  :PrimitiveRecursiveFunction;
  s:seeAlso :boundedBy.

:boundedBy s:label "bounded by";
  s:domain :PrimitiveRecursiveFunction;
  s:range  :Natural;
  s:comment """We can start testing 0,1,2,3... but set an upper bound to our search. We search until we hit the upper bound and then stop. If we find a value before stopping which makes f(x) = 0, then g returns that value; if not, then g returns 0. This is called bounded minimization.""".

{ :g :minimizes :f.
  "0" :f "0".
  :y a :Natural.
} log:implies { :y :g "0" }.

{ :y a :Natural; :s :sy.
  "0" :f :sy.
  :z a :Natural.
}
  log:implies { :f :notZeroAt "0"; :whenBoundedBy :z }.

{ :f :notZeroAt :x; :whenBoundedBy :z.
  :y a :Natural; :s :sy.
  :x :s :sx.
  :sx :lessThan :z.
  :sx :f :sy.
}
  log:implies { :f :notZeroAt :sx; :whenBoundedBy :z }.

{ :g :minimizes :f; :boundedBy :z.
  :f :notZeroAt :x; :whenBoundedBy :z.
  :x :s :sx.
  :sx :f "0".
  :y a :Natural.
}
  log:implies { :y :g :sx }.


:s s:subPropertyOf :lessThan.
:lessThan s:label "less than", "<";
  a :_TransitiveProperty;
  s:domain :Natural;
  s:range :Natural.

#### a little bit of DAML+OIL...
{ :f a :_TransitiveProperty.
  :x :f :y.
  :y :f :z.
}
  log:implies { :x :f :z }.

:TODO s:subPropertyOf dc:description.
<> :TODO """@@didn't actually get around to the induction rule,
   which is where all the power is.""".

:rcsLog s:subPropertyOf dc:description.

<> :rcsLog """
$Log: pra.n3,v $
Revision 1.2  2002/01/24 21:33:16  connolly
noted the omission of the unduction rule.

""".