Loading...
Please wait, while we are loading the content...
Similar Documents
Consistently Adding Primitive Recursive Definitions in ACL2 (2002)
| Content Provider | CiteSeerX |
|---|---|
| Author | Cowles, John |
| Abstract | In [2, 3], P. Manolios and J Moore show that a tail recursive defining equation for a new function can always be consistently added to ACL2. This is done by “constructing ” a function that satisfies the proposed tail recursive defining equation. Their construction is extended to many primitive recursive defining equations. This extends the known recursive schemes that can be consistently introduced into ACL2’s logic. Exactly what is meant by “primitive recursive ” and the exact restrictions placed on the definitions are explained below. 1 Tail Recursion P. Manolios and J Moore [2, 3] describe a macro named defpun for consistently introducing “partial functions ” into ACL2. One of the many cases handled by defpun is when the “defining equation ” is tail recursive: Let test, base, and st be arbitrary unary functions. There always is an ACL2 function f that satisfies (equal (f x) |
| File Format | |
| Publisher Date | 2002-01-01 |
| Access Restriction | Open |
| Subject Keyword | Adding Primitive Recursive Definition Tail Recursive Exact Restriction Acl2 Function Partial Function Many Case Known Recursive Scheme Primitive Recursive New Function Arbitrary Unary Function Tail Recursion Many Primitive Recursive |
| Content Type | Text |
