Recursively defined domains and their induction principles

AbstractRecursion is one of the main tools in denotational semantics. This paper deals with the problem of establishing induction principles for domains defined by simultaneous recursion. We are particularly interested in induction principles supporting verification of properties of elements from (any) one of the domains defined by the simultaneous recursion. We offer two such principles, with the second principle being especially well-suited for implementation in a machine system such as LCF [5]