Tarski's fixed-point theorem and lambda calculi with monotone inductive types
Ralph Matthes
Synthese 133(1), 107-129 (October 2002)
The new concept of lambda calculi with monotone inductive types is introduced by help of motivations drawn from Tarski's fixed-point theorem (in preorder theory) and initial algebras and initial recursive algebras from category theory. They are intended to serve as formalisms for studying iteration and primitive recursion on general inductively given structures. Special accent is put on the behaviour of the rewrite rules motivated by the categorical approach, most notably on the question of strong normalization (i. e., the impossibility of an infinite sequence of successive rewrite steps). It is shown that this key property hinges on the concrete formulation. The canonical system of monotone inductive types, where monotonicity is expressed by a monotonicity witness being a term expressing monotonicity through its type, enjoys strong normalization shown by an embedding into the traditional system of non-interleaving positive inductive types which, however, has to be enriched by the parametric polymorphism of system F. Restrictions to iteration on monotone inductive types already embed into system F alone, hence clearly displaying the difference between iteration and primitive recursion with respect to algorithms despite the fact that, classically, recursion is only a concept derived from iteration.
Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T
Felix Joachimski and Ralph Matthes
Archive for Mathematical Logic 42 (2003) 1, 59-87.
Inductive characterizations of the sets of terms, the subset of strongly normalizing terms and normal forms are studied in order to reprove weak and strong normalization for the simply-typed lambda-calculus and for an extension by sum types with permutative conversions. The analogous treatment of a new system with generalized applications inspired by von Plato's generalized elimination rules in natural deduction shows the flexibility of the approach which does not use the strong computability/candidate style à la Tait and Girard. It is also shown that the extension of the system with permutative conversions by eta-rules is still strongly normalizing, and likewise for an extension of the system of generalized applications by a rule of "immediate simplification". By introducing an infinitely branching inductive rule the method even extends to Gödel's T.
Monotone Inductive and Coinductive Constructors of Rank 2
Ralph Matthes
In the Proceedings of CSL 2001, Lecture Notes in Computer Science Vol. 2142, © Springer Verlag
A generalization of positive inductive and coinductive types to monotone inductive and coinductive constructors of rank 1 and rank 2 is described. The motivation is taken from initial algebras and final coalgebras in a functor category and the Curry-Howard-correspondence. The definition of the system as a lambda-calculus requires an appropriate definition of monotonicity to overcome subtle problems, most notably to ensure that the (co-)inductive constructors introduced via monotonicity of the underlying constructor of rank 2 are also monotone as constructors of rank 1. The problem is solved, strong normalization shown, and the notion proven to be wide enough to cover even highly pathological examples.
Interpolation for natural deduction with generalized eliminations
Ralph Matthes
In the Proceedings of PTCS 2001 (Proof Theory in Computer Science), Lecture Notes in Computer Science Vol. 2183, © Springer Verlag
A modification of simply-typed lambda-calculus by generalized elimination rules in the style of von Plato is presented. Its characteristic feature are permutative conversions also for function types and product types. After the addition of certain extensional reduction rules, an interpolation theorem (à la Lyndon) is proven which is also aware of the terms (a.k.a. the proofs via the Curry-Howard-isomorphism) like in Cubric's treatment of the usual lambda-calculus. Connections between interpolation and canonical liftings of positive and negative type dependencies are given which are important for the intensional treatment of inductive datatypes.
Parigot's Second Order Lambda-Mu-Calculus and Inductive Types
Ralph Matthes
In the Proceedings of TLCA 2001, Lecture Notes in Computer Science Vol. 2044, © Springer Verlag
A new proof of strong normalization of Parigot's (second order) lambda-mu-calculus is given by a reduction-preserving embedding into system F (second order polymorphic lambda-calculus). The main idea is to use the least stable supertype for any type. These non-strictly positive inductive types and their associated iteration principle are available in system F, and allow to give a translation vaguely related to CPS translations (corresponding to the Kolmogorov embedding of classical logic into intuitionistic logic). However, they simulate Parigot's mu-reductions whereas CPS translations hide them.
As a major advantage, this embedding does not use the idea of reducing stability (not not phi -> phi) to that for atomic formulae. Therefore, it even extends to non-interleaving positive fixed-point types. As a non-trivial application, strong normalization of lambda-mu-calculus, extended by primitive recursion on monotone inductive types, is established.
Characterizing Strongly Normalizing Terms for a Lambda Calculus with Generalized Applications via Intersection Types
Ralph Matthes
In the Proceedings of the Satellite Workshops of the 27th International Colloquium on Automata, Languages, and Programming, Geneva, Switzerland (Carleton Scientific)
An intersection type assignment system for the extension LambdaJ of the untyped lambda-calculus, introduced by Joachimski and Matthes, is given and proven to characterize the strongly normalizing terms of LambdaJ. Since LambdaJ's generalized applications naturally allow permutative/commuting conversions, this the first analysis of a term rewrite system with permutative conversions by help of intersection types. Two proofs are given for the fact that the typable terms are strongly normalizing: One by the computability predicates method a la Tait and one showing directly that strongly normalizing typable terms are closed under (generalized) application and substitution. It is also shown that a straightforward extension of the type assignment for lambda calculus fails to capture the strongly normalizing terms.
Standardization and Confluence for a Lambda Calculus with Generalized Applications
Felix Joachimski and Ralph Matthes
In the Proceedings of the RTA 2000, Rewriting Techniques and Applications, 11th International Conference, Norwich, UK, July 10-12, Lecture Notes in Computer Science Vol. 1833, © Springer Verlag
The following is an expansion of the abstract:
As a minimal environment for the study of permutative reductions an extension LambdaJ of the untyped lambda-calculus is considered. In this non-terminating system with non-trivial critical pairs, confluence is established by studying triangle properties that allow to treat permutative reductions modularly and could be extended to more complex term systems with permutations. Standardization is shown by means of an inductive definition of standard reduction that closely follows the inductive term structure and captures the intuitive notion of standardness even for permutative reductions.
- The calculus LambdaJ extends lambda-calculus by a generalized application rS that gives rise to permutative conversions of the form (rS)T -> r(S{T}) already in the untyped, non-normalizing setting. It can be understood as the closure of the computational content of cut-free LJ (Gentzen's intuitionistic sequent calculus) under substitution. For a short description and a proof of strong normalization of the simply typed version see the paper Short proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T by the same authors.
- Confluence in LambdaJ does not follow from standard higher order rewriting theory, since permutative conversions lead to non-trivial critical pairs that are not development-closed (not even almost). However, permutations always converge and the interaction between beta-reduction and permutation is not too intricate. This allows to prove a commutation property between beta-developments and permutation. Using sequential composition (instead of the union) of those two relations, a development for the combined reduction relation is established, and confluence ensues.
- The concept of standard reduction sequence is difficult to define by the usual notion of proceeding left-to-right in the term string representation. Therefore an inductive definition ~> of standard reduction is used that closely follows the inductive term structure in a canonical way and captures the intuitive notion of standardness even for permutative reductions. The standardization theorem states ~> = ->* and thereby yields a new induction principle for ->*. As a prototypical application a syntax-directed inductive characterization of the weakly normalizing terms of LambdaJ is proved.
Monotone (co)inductive types and positive fixed-point types
Ralph Matthes
Theoretical Informatics and Applications (33) 4/5, 309-328, 1999
We study five extensions of the polymorphically typed lambda-calculus (system F) by type constructs intended to model fixed-points of monotone operators. Building on work by H. Geuvers concerning the relation between term rewrite systems for least pre-fixed-points and greatest post-fixed-points of positive type schemes (i. e., non-nested positive inductive and coinductive types) and so-called retract types, we show that there are type-respecting and reduction-preserving embeddings even between systems of monotone (co)inductive types and non-interleaving positive fixed-point types (which are essentially those retract types). The reduction relation considered is beta- and eta-reduction for system F plus either (full) primitive recursion on the inductive types or (full) primitive corecursion on the coinductive types or an extremely simple rule for the fixed-point types. Monotonicity is not reduced to the syntactic restriction of only positive occurrences of the type variable alpha in rho when forming the inductive type "mu alpha rho" or the coinductive type "nu alpha rho". Instead only a monotonicity witness which is a term of type "forall alpha forall beta.(alpha->beta)->rho->rho[alpha:=beta]" is required. This term may already use (co)recursion such that our monotone (co)inductive types may even be interleaved and not only nested.
Monotone Fixed-Point Types and Strong Normalization
Ralph Matthes
In the Proceedings of the CSL '98, Computer Science Logic, 12th International Workshop, Brno, Czech Republic, August 24-28, Lecture Notes in Computer Science Vol. 1584, © Springer Verlag
Several systems of fixed-point types (also called retract types or recursive types with explicit isomorphisms) extending system F are considered. The seemingly strongest systems have monotonicity witnesses and use them in the definition of beta reduction for those types. A more naive approach leads to non-normalizing terms. All the other systems are strongly normalizing because they embed in a reduction-preserving way into the system of non-interleaved positive fixed-point types which can be shown to be strongly normalizing by an easy extension of some proof of strong normalization for system F.
Functoriality of monotonicity witnesses in the system of positive (interleaved) inductive types
Ralph Matthes
Abstract of my talk at the Logic Colloquium 1998 in the Bulletin of Symbolic Logic Vol. 5(1), March 1999
There is no abstract of the abstract available.
Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types
Ralph Matthes
The PhD thesis has been submitted in May 1998.
There is no short abstract yet. Please read pages 1 - 8 (the introduction).
Convergence of Causal Probabilistic Networks
Ralph Matthes and Ulrich G. Oppel
In the book "Uncertainty in Intelligent Systems", Elsevier Science Publishers B.V., 1993.
Sorry. No abstract available.
Home Page
TCS
Computer Science Institute
University