Partial and Nested Recursive Function Definitions in Higher-order Logic |
| |
Authors: | Alexander Krauss |
| |
Affiliation: | 1.Institut für Informatik,Technische Universit?t München,Munich,Germany |
| |
Abstract: | Based on inductive definitions, we develop a tool that automates the definition of partial recursive functions in higher-order
logic (HOL) and provides appropriate proof rules for reasoning about them. Termination is modeled by an inductive domain predicate
which follows the structure of the recursion. Since a partial induction rule is available immediately, partial correctness
properties can be proved before termination is established. It turns out that this modularity also facilitates termination
arguments for total functions, in particular for nested recursions. Our tool is implemented as a definitional package extending
Isabelle/HOL. Various extensions provide convenience to the user: pattern matching, default values, tail recursion, mutual
recursion and currying. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|