The logic of recursive equations

Publisher Website
Google Scholar
Abstract
We study logical systems for reasoning about equations involving recursive definitions. In particular, we are interested in “propositional” fragments of the functional language of recursion FLR [18, 17], i.e., without the value passing or abstraction allowed in FLR. The “pure,” propositional fragment FLR0 turns out to coincide with the iteration theories of [1]. Our main focus here concerns the sharp contrast between the simple class of valid identities and the very complex consequence relation over several natural classes of models.

This publication has 6 references indexed in Scilit: