A recursion principle for linear orderings

1992 ◽  
Vol 57 (1) ◽  
pp. 82-96 ◽  
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.

scholarly journals Final coalgebras as greatest fixed points in ZF set theory

1999 ◽  
Vol 9 (5) ◽  
pp. 545-567 ◽  
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).

scholarly journals Recursive Definitions and Fixed-Points

2009 ◽  
Vol 247 ◽  
pp. 19-37 ◽  
Author(s):  
Francicleber Martins Ferreira ◽  
Ana Teresa Martins
Keyword(s):  
Fixed Points ◽  
Recursive Definitions

GAME FORMATS AS CHU SPACES

2007 ◽  
Vol 09 (01) ◽  
pp. 119-138 ◽  
Author(s):  
STEFANO VANNUCCI
Keyword(s):  
Suitable Choice ◽  
Coalitional Game ◽  
Extensive Game ◽  
Game Theoretic ◽  
Chu Spaces ◽  
Natural Way

It is argued that when morphisms are ignored virtually all coalitional, strategic and extensive game formats as currently employed in the extant game-theoretic literature may be presented in a fairly natural way as (concrete categories over) discrete subcategories of Chu(Set,2). Moreover, under a suitable choice of coalitional morphisms, coalitional game formats are shown to be (concrete categories over) full subcategories of Chu(Set,2).

scholarly journals Fixed Points on Abstract Structures without the Equality Test

2002 ◽  
Vol 9 (26) ◽  
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.

scholarly journals 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.

scholarly journals On fixed points of the lower set operator

2015 ◽  
Vol 25 (01n02) ◽  
pp. 259-292 ◽  
Author(s):  
J. Almeida ◽  
A. Cano ◽  
O. Klíma ◽  
J.-É. Pin
Keyword(s):  
Fixed Points ◽  
Semigroup Theory ◽  
Ordered Semigroup ◽  
Ordered Semigroups ◽  
Large Families ◽  
Natural Way

Lower subsets of an ordered semigroup form in a natural way an ordered semigroup. This lower set operator gives an analogue of the power operator already studied in semigroup theory. We present a complete description of the lower set operator applied to varieties of ordered semigroups. We also obtain large families of fixed points for this operator applied to pseudovarieties of ordered semigroups, including all examples found in the literature. This is achieved by constructing six types of inequalities that are preserved by the lower set operator. These types of inequalities are shown to be independent in a certain sense. Several applications are also presented, including the preservation of the period for a pseudovariety of ordered semigroups whose image under the lower set operator is proper.

Minimal models

1977 ◽  
Vol 42 (2) ◽  
pp. 254-260
Author(s):  
Rainer Deissler
Keyword(s):  
Upper Bound ◽  
Minimal Models ◽  
First Order ◽  
Elementary Submodel ◽  
Game Theoretic ◽  
Theoretic Characterization ◽  
Natural Way

A model is called minimal if it does not contain a proper elementary submodel. A class of models is called Σ11(Π11 resp. elementary) if it is axiomatized by a sentence with σ in and some string of predicate symbols. All languages considered are assumed to be countable. For each model we shall define in a natural way its rank, denoted by rk (), which is an ordinal or ∞. Intuitively speaking, rk () is the least upper bound for the number of steps needed to define the elements of by first order formulas; e.g. we shall have rk((ω, <)) = 1 (each element is f.o. definable), rk ((Z, <)) = 2 (no element is f.o. definable, each element is f.o. definable using any other element as a parameter), rk ((Q, <) ) = ∞ (no element is f.o. definable by any number of steps). This notion of rank leads to a useful game theoretic characterization of minimal models which we apply to show that the Π11 class of minimal models is not Σ11.

scholarly journals Recursive definitions and fixed-points on well-founded structures

2011 ◽  
Vol 412 (37) ◽  
pp. 4893-4904
Author(s):  
Francicleber Martins Ferreira ◽  
Ana Teresa Martins
Keyword(s):  
Fixed Points ◽  
Recursive Definitions

scholarly journals Representing Continuous Functions between Greatest Fixed Points of Indexed Containers

2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Pierre Hyvernat
Keyword(s):  
Fixed Points ◽  
Type Theory ◽  
Continuous Functions ◽  
Dependent Type Theory ◽  
Recursive Definitions ◽  
Computable Functions ◽  
Dependent Type

We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types. Those transducers can be defined in dependent type theory without any notion of equality but require inductive-recursive definitions. Most of the properties of these constructions only rely on a mild notion of equality (intensional equality) and can thus be formalized in the dependently typed language Agda.

Sign in / Sign up

Export Citation Format

Share Document