arXiv subjects
Publications and source records attributed to Daniel Leivant.
We show that a partial-correctness assertion about an iterative program is provable in Hoare Logic iffit is provable in standard second-order logic with comprehension restricted to first-order predicates. This equivalence was claimed twice in the past, both with faulty proofs, and seems to be the first foundational characterization of Hoare Logic.
The ramification method in Implicit Computational Complexity has been associated with functional programming, but adapting it to generic imperative programming is highly desirable, given the wider algorithmic applicability of imperative programming. We introduce a new approach to ramification which, among other benefits, adapts readily to fully general imperative programming. The novelty is in ramifying finite second-order objects, namely finite structures, rather than ramifying elements of free algebras. In so doing we bridge between Implicit Complexity's type theoretic characterizations of feasibility, and the data-flow approach of Static Analysis.
We develop a novel formal theory of finite structures, based on a view of finite structures as a fundamental artifact of computing and programming, forming a common platform for computing both within particular finite structures, and in the aggregate for computing over infinite data-types construed as families of finite structures. A "finite structure" is here a finite collection of finite partial-functions, over a common universe of atoms. The theory is second-order, as it uses quantification over finite functions. Our formal theory FS uses a small number of fundamental axiom-schemas, with finiteness enforced by a schema of induction on finite partial-functions. We show that computability is definable in the theory by existential formulas, generalizing Kleene's Theorem on the Sigma-1 definability of RE sets, and use that result to prove that FS is mutually interpretable with Peano Arithmetic.
Implicit computational complexity, which aims at characterizing complexity classes by machine-independent means, has traditionally been based, on the one hand, on programs and deductive formalisms for free algebras, and on the other hand on descriptive tools for finite structures. We consider here "uninterpreted" programs for the transformation of finite structures, which define functions over a free algebra A once the elements of A are themselves considered as finite structures. We thus bridge the gap between the two approaches above to implicit complexity, with the potential of streamlining and clarifying important tools and techniques, such as set-existence and ramification. We illustrate this potential by delineating a broad class of programs, based on the notion of loop variant familiar from imperative program construction, that characterizes a generic notion of primitive-recursive complexity, without reference to any data-driven recurrence.
We propose a framework for reasoning about programs that manipulate coinductive data as well as inductive data. Our approach is based on using equational programs, which support a seamless combination of computation and reasoning, and using productivity (fairness) as the fundamental assertion, rather than bi-simulation. The latter is expressible in terms of the former. As an application to this framework, we give an implicit characterization of corecurrence: a function is definable using corecurrence iff its productivity is provable using coinduction for formulas in which data-predicates do not occur negatively. This is an analog, albeit in weaker form, of a characterization of recurrence (i.e. primitive recursion) in [Leivant, Unipolar induction, TCS 318, 2004].