Def x! == if x= 0
1 else x
(x-1)! fi (recursive)
where
?= is a?
-valued test of integer equality.
Here's an example of how it evaluates:
3! * 3
(3-1)! *
3
2
(3-1-1)! *
3
2
1
(3-1-1-1)! *
3
2
1
1 *
6
Observe that execution
(-1)! * , et cetera.(-1)
(-1-1)! *
(-1)
(-1-1)
(-1-1-1)!
The argument that x:
. x!
The potential and convenience of general recursion is better demonstrated with the following variant of factorial that has a result only on non-negative even inputs.
Def x! == if x=
0
1 else x
(x-2)!
fi (recursive)
Thm* x:{x:
| (x rem 2) = 0 }. x!
![]()
![]()
Indeed, one can even type Kleene's paradigmatic unbounded search function,
Def mu(f) == if f(0) 0 else 1+mu(
x.f(1+x)) fi (recursive)
Thm* mu {f:(
)|
x:
. f(x) }
Thm* f:{f:(
)|
x:
. f(x) }. f(mu(f))
Thm* f:{f:(
)|
x:
. f(x) }, i:
. i<mu(f)
![]()
f(i)
(See also
One can also define type-valued functions and predicates by general recursion on the domain. Here is a definition of
Note: this is not a recursive type, but a recursive definition of a family of types. See
Def A^n == if n= 0
Unit ; n=
1
A else A
(A^(n-1)) fi (recursive)
Thm* A:Type, n:
. (A^n)
Type
Now let us compute:
A^0 * Unit
A^1 * A
A^2 * A
A
A^3 * A
A
A
Here's a predicate on
Def u in X: A^n. P(u)
Def == n = 1![]()
& P(X)
n
2 & (X/a,rest. P(a)
(
u in rest: A^(n-1). P(u)))
Def (recursive)
Thm* A:Type, P:(A
Prop), n:
, X:(A^n). (
u in X: A^n. P(u))
Prop
Example of use:
Thm* i in <1,(-1),0>:
^3. i<0
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() |