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

Postscript 289Kb |

## Abstract

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