Loading...
Please wait, while we are loading the content...
Similar Documents
Partial functions in ACL2 (2003)
| Content Provider | CiteSeerX |
|---|---|
| Author | Manolios, Panagiotis Moore, J. Strother |
| Abstract | We describe a method for introducing “partial functions ” into ACL2, i.e., functions not defined everywhere. The function “definitions ” are actually admitted via the encapsulation principle: the new function symbol is constrained to satisfy the appropriate equation. This is permitted only when a witness function can be exhibited, establishing that the constraint is satisfiable. Of particular interest is the observation that every tail recursive definition can be witnessed in ACL2. We describe a macro that allows the convenient introduction of arbitrary tail recursive functions and we discuss how such functions can be used to prove theorems about state machine models without reasoning about “clocks ” or counting the number of steps until termination. Our macro for introducing “partial functions ” also permits a variety of other recursive schemes and we briefly illustrate some of them. 1. |
| File Format | |
| Volume Number | 31 |
| Journal | Journal of Automated Reasoning |
| Language | English |
| Publisher Date | 2003-01-01 |
| Access Restriction | Open |
| Subject Keyword | Partial Function Particular Interest Convenient Introduction Tail Recursive Definition Arbitrary Tail Recursive Function Appropriate Equation Function Definition Witness Function State Machine Model Recursive Scheme New Function Symbol Encapsulation Principle |
| Content Type | Text |
| Resource Type | Article |
