fixpoints

personoj/examples/fixpoints.lp

+require open personoj.lhol personoj.nat personoj.extra.fixpoints personoj.logical;
+
+symbol mul : Nat → Nat → Nat;
+symbol pred : Nat → Nat;
+symbol pred-lower: Prf (∀ {nat/o}(λ n, (lenat (pred n) n)));
+
+// Definition of the factorial
+symbol fac n ≔
+  fix nat/o nat/o (λ x, x)
+      (λ n fac,
+       if (eqnat n zero)
+          (λ _, zero)
+          (λ _, (mul n (fac (pred n) (pred-lower n))))) n;

personoj/extra/fixpoints.lp

+require open personoj.lhol personoj.nat;
+
+// Basic fixpoint with a measure
+symbol fix (a: Set)(r: Set)(meas:El a → Nat)
+           (f: Π(x:El a),
+               (Π(y:El a)(π:Prf(lenat (meas y) (meas x))), El r) → El r):
+  El a → El r;
+rule fix $a $r $meas $f $x ↪
+     $f $x
+        (λ (y: El $a) (π:Prf(lenat ($meas y) ($meas $x))),
+         fix $a $r $meas $f y);

personoj/nat.lp

@@ -10,6 +10,12 @@ with eqnat zero (succ _) ↪ false
 with eqnat (succ _) zero ↪ false
 with eqnat zero zero ↪ true;
 
+symbol lenat: Nat → Nat → Prop;
+rule lenat zero zero ↪ false
+with lenat (succ _) zero ↪ false
+with lenat zero (succ _) ↪ true
+with lenat (succ $n) (succ $m) ↪ lenat $n $m;
+
 // Recursor on integers
 symbol nrec {t: Set} : Nat → El t → (Nat → El t → El t) → El t;
 rule nrec {$t} (succ $n) $base $f ↪ $f $n (nrec {$t} $n $base $f);