It is well-known that concepts and methods of logic (more specifically constructive logic) occupy a central place in computer science. While it is quite common to identify 'logic' with 'first-order logic' (FOL), a careful examination of the various applications of logic in computer science reveals that FOL is insufficient for most of them, and that its most crucial shortcoming is its inability to provide inductive definitions in general, and the notion of the transitive closure in particular. The minimal logic that can serve for this goal is ancestral logic (AL). In this paper we define a constructive version of AL, pure intuitionistic ancestral logic (iAL), extending pure intuitionistic first-order logic (iFOL). This logic is a dependently typed abstract programming language with computational functionality beyond iFOL, given by its realizer for the transitive closure operator TC, which corresponds to recursive programs. We derive this operator from the natural type theoretic definition of TC using intersection type. We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory. We further outline how iAL can serve as a natural framework for reasoning about programs.
展开▼
