article · 1991
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive
Nora Szasz
Cited by 0Abstract and details only
Abstract
Specification Approach As is common in programming, it is possible in ALF to work with abstract sets and operations rather than with their actual inductive and recursive definitions. Thus, we may specify abstract structures and operations, which consist of a collection of propositions implicitly characterizing a number of sets and operations on them (such a specification is usually given by a set of equations). When writing the proof, we used this approach in order to work in a modular style, and so, independently from the exact definitions of some sets and propositions. The usual definition of tuples, for instance, is given by requiring (a family of) sets T(n) for n ffl N, having the following operations: nil ffl T(0), cons: N \\Theta T(n) ! T(succ(n)), for all n ffl N, hd: T(succ(n)) ! N, for all n ffl N, tl: T(succ(n)) ! T(n), for all n ffl N, such that the following equalities hold: hd(cons(a; t))= a, for all a ffl N, t ffl T(n) (n ffl N), tl(cons(a; t))= t, for all a ffl N, t f...
Cite this paper
Szasz, N. (1991). A Machine Checked Proof that Ackermann's Function is not Primitive Recursive.
Szasz, Nora. “A Machine Checked Proof that Ackermann's Function is not Primitive Recursive.” 1991.
Szasz, Nora. 1991. “A Machine Checked Proof that Ackermann's Function is not Primitive Recursive.”
Szasz, N. (1991) ‘A Machine Checked Proof that Ackermann's Function is not Primitive Recursive’.
@article{szasz1991machine,
title = {{A Machine Checked Proof that Ackermann's Function is not Primitive Recursive}},
author = {Szasz, Nora},
year = {1991}
}Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.