A finitary version of the calculus of partial inductive definitions

Eriksson, Lars-Henrik (1992) A finitary version of the calculus of partial inductive definitions. [SICS Report]



The theory of partial inductive definitions is a mathematical formalism which has proved to be useful in a number of different applications. The fundamentals of the theory is shortly described. Partial inductive definitions and their associated calculi are essentially infinitary. To implement them on a computer, they must be given a formal finitary representation. We present such a finitary representation, and prove its soundness. The finitary representation is given in a form with and without variables. Without variables, derivations are unchanging entities. With variables, derivations can contain logical variables that can become bound by a binding environment that is extended as the derivation is constructed. The variant with variables is essentially a generalization of the pure GCLA programming language.

Item Type:SICS Report
ID Code:2112
Deposited By:Vicki Carleson
Deposited On:22 Oct 2007
Last Modified:18 Nov 2009 16:00

Repository Staff Only: item control page