Recursive Definitions and Fixed-Points

Final coalgebras as greatest fixed points in ZF set theory

Mathematical Structures in Computer Science ◽

10.1017/s0960129599002790 ◽

1999 ◽

Vol 9 (5) ◽

pp. 545-567 ◽

Cited By ~ 3

Author(s):

LAWRENCE C. PAULSON

Keyword(s):

Fixed Points ◽

Set Theory ◽

Theorem Prover ◽

Infinite Length ◽

Special Cases ◽

Definition Of ◽

Recursive Definitions ◽

Ordered Pairs

A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo–Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel's solution and substitution lemmas are proved in the style of Rutten and Turi (1993). The approach is less general than Aczel's, but the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint.Compared with previous work (Paulson, 1995a), iterated substitutions and solutions are considered, as well as final coalgebras defined with respect to parameters. The disjoint sum construction is replaced by a smoother treatment of urelements that simplifies many of the derivations.The theory facilitates machine implementation of recursive definitions by letting both inductive and coinductive definitions be represented as fixed points. It has already been applied to the theorem prover Isabelle (Paulson, 1994).

Download Full-text

Fixed Points on Abstract Structures without the Equality Test

BRICS Report Series ◽

10.7146/brics.v9i26.21742 ◽

2002 ◽

Vol 9 (26) ◽

Cited By ~ 1

Author(s):

Margarita Korovina

Keyword(s):

Fixed Points ◽

Recursive Definitions ◽

Equality Test ◽

Effective Operators

In this paper we present a study of definability properties of fixed points of effective operators on abstract structures without the equality test. In particular we prove that Gandy theorem holds for abstract structures. This provides a useful tool for dealing with recursive definitions using Sigma-formulas.<br /> <br />One of the applications of Gandy theorem in the case of the reals without the equality test is that it allows us to define universal Sigma-predicates. It leads to a topological characterisation of Sigma-relations on |R.

Download Full-text

Monotone Relations, Fixed Points and Recursive Definitions

Towards Mathematical Philosophy ◽

10.1007/978-1-4020-9084-4_7 ◽

2008 ◽

pp. 125-164

Author(s):

Janusz Czelakowski

Keyword(s):

Fixed Points ◽

Recursive Definitions

Download Full-text

A recursion principle for linear orderings

Journal of Symbolic Logic ◽

10.2307/2275177 ◽

1992 ◽

Vol 57 (1) ◽

pp. 82-96 ◽

Cited By ~ 2

Author(s):

Juha Oikkonen

Keyword(s):

Fixed Points ◽

Initial Segment ◽

Theoretical Methods ◽

Linear Orderings ◽

Direct Limits ◽

Game Theoretic ◽

Recursive Definitions ◽

Natural Way

AbstractThe idea of this paper is to approach linear orderings as generalized ordinals and to study how they are made from their initial segments. First we look at how the equality of two linear orderings can be expressed in terms of equality of their initial segments. Then we shall use similar methods to define functions by recursion with respect to the initial segment relation. Our method is based on the use of a game where smaller and smaller initial segments of linear orderings are considered. The length of the game is assumed to exceed that of the descending sequences of elements of the linear orderings considered. By use of such game-theoretical methods we can for example extend the recursive definitions of the operations of sum, product and exponentiation of ordinals in a unique and natural way for arbitrary linear orderings. Extensions coming from direct limits do not satisfy our game-theoretic requirements in general. We also show how our recursive definitions allow very simple constructions for fixed points of functions, giving rise to certain interesting linear orderings.

Download Full-text

Recursive Definitions of Monadic Functions

10.29007/1mdt ◽

2018 ◽

Author(s):

Alexander Krauss

Keyword(s):

Fixed Points ◽

The State ◽

Recursive Functions ◽

Recursion Equation ◽

Recursive Definitions ◽

Standard Domain

Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a convenient definition principle for imperative programs, which were previously hard to define.For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically.

Download Full-text