We solve the problem of defining generalized iteration (generalized in the direction of generalized folds by Bird and Paterson) and its dual for inductive and coinductive constructors (nested datatypes) of {\em arbitrary} rank by appropriately generalizing Mendler-style (co)iteration. Characteristically to Mendler-style schemes of disciplined (co)recursion, the schemes we propose do not rest on notions like positivity or monotonicity of a constructor and facilitate programming in a natural and elegant style close to programming with the customary \texttt{letrec} construct, where the typings of the schemes, however, guarantee termination. For rank~2, a smoothened version of Bird and Paterson's generalized folds and its dual are achieved, for rank 1, the schemes instantiate to Mendler's original (re)formulation of iteration and coiteration. Several examples demonstrate the power of the approach. Strong normalization of our proposed extension of system~$\Fomega$ of higher-order parametric polymorphism is proven by a reduction-preserving embedding into pure~$\Fomega$.
Participant: Klaus Aehlig
Talk: Types for Finitely Iterated Inductive Definitions
Abstract:
We consider the fragment of the polymorphic lambda calculus (``System F'') where all types are built (up to alpha-conversion) from a single type variable only. This fragment is expressible enough for most ``real world'' data structures including the finite tree classes. It is shown how this fragment can be reduced to finitely iterated inductive definitions.
Participant: Thorsten Altenkirch
Participant: Gilles Barthe
Participant: Ulrich Berger
Participant: Yves Bertot
We describe the operational and denotational semantics of a small
imperative language in type theory with inductive and recursive
definitions. The operational semantics is given by natural inference
rules, implemented as an inductive relation. The realization of the
denotational semantics is more delicate: The nature of the language
imposes a few difficulties on us. First, the language is
Turing-complete, and therefore the interpretation function we consider
is necessarily partial. Second, the language contains strict
sequential operators, and therefore the function necessarily exhibits
nested recursion. Our solution combines and extends recent work by
the authors and others on the treatment of general recursive functions
and partial and nested recursive functions. The first new result is a
technique to encode the approach of Bove and Capretta for partial and
nested recursive functions in type theories that do not provide
simultaneous induction-recursion.
A second result is a clear understanding of the characterization of
the definition domain for general recursive functions, a key aspect in
the approach by iteration of Balaa and Bertot. In this respect, the
work on operational semantics is a meaningful example, but the
applicability of the technique should extend to other circumstances
where complex recursive functions need to be described formally.
Participant: Frederic Blanqui
I will present general syntactic conditions ensuring the strong
normalization of the Calculus of Constructions extended with functions
and predicates defined by higher-order rewrite rules.
Participant: Ana Bove (joint work with Venanzio Capretta)
General recursive algorithms satisfy no syntactic condition that
guarantees termination and therefore there is no direct way of
formalising such algorithms in type theory. On the other hand,
functional programming impose no restrictions on recursive programs,
and then writing a general recursive algorithm is straightforward.
However, there is no powerful framework that allows us to reason about
the correctness of functional programs.
The goal of this talk is to present a method that combines the
advantages of both programming styles when formalising general
recursive algorithms. In this way, a short algorithm that can be
proven correct by using the expressive power of type theory would be
obtained.
Participant: Venanzio Capretta
The talk presents a formalization of partial recursive functions in Type
Theory. To every type A we associate a coinductive type A' of possibly
infinite computations of type A. A recursive function from A to B is
represented by an element of A -> B'.
Participant: Pietro Di Gianantonio (joint work with Marino Miculan)
In type theory based logical frameworks, recursive and co-recursive
definitions are subject to syntactic restrictions that ensure their
termination and productivity. These restrictions however greately
decrease the expressive power of the language. In this work we
propose a general approach for systematically defining fixed points
for a broad class of well given recursive definition. This approach
unifies the ones based on well-founded order to the ones based on
complete metrics and contractive functions, thus allowing for
mixed recursive/corecursive definitions. The resulting
theory, implemented in the Coq proof assistant, is quite simple and
hence it can be used broadly with a small, sustainable overhead on the
user.
Participant: Arne John Glenstrup
Participant: Felix Joachimski
We give a detailed analysis of the interaction between beta-reduction
and eta-expansion in the simply-typed lambda-calculus that leads to a
modular and purely syntactic proof of strong normalization of the
combination of the two reductions. It is shown how this technique
extends to beta-normalizing functional Pure Type Systems with a
restricted variant of Barthe's formulation of eta-expansion.
Participant: Ralph Matthes
Participant: Conor McBride (joint work with James McKinna)
Many algorithms of much less complexity than a bootstrapping
interpreter fail, at first glance, to fit the restrictive paradigm of
`structural recursion', in which termination is guaranteed by
typechecking. The reason is that the structures of these algorithms
are not visible in the programs which implement them. The traditional
`separation of concerns' approach to this problem is to recover these
structures `after the fact' by ad hoc termination proofs. However,
dependent types can equip data with much more visible structure. This
suggests that we should also consider the possibility of implementing
algorithms by new programs which make enough of their structure
visible to get termination `for free'.
Participant: James McKinna (joint work with Conor McBride)
Participant: Tarmo Uustalu
Uustalu, Vene and Pardo and Bartels have shown that a number of
seemingly unrelated advanced disciplined recursion schemes are
instances of a generic scheme parameterized by a comonad and a
distributive law of the base functor of the inductive type of interest
over the comonad. What is more, it even suffices to have a functor
instead of the comonad; in that case, a comonad (the cofree comonad of
the functor) shows up in the background. It makes sense to try to
support these semantically justified generic schemes in a typed lambda
calculus via language primitives. This, however, is a bit tricky,
since the straightforward codings employing positivity or monotonicity
of a type constructor are not really elegant. We show that
N. P. Mendler's approach to coding disciplined recursion schemes, in
which neither notion is needed, is fruitfully applicable also to
comonad-specified recursion.
Participant: Paul J. Voda
Beside the obvious gains of having a good declarative semantics for
the programming language (Why to integrate otherwise?) and of
computer-aided proofs of properties of programs (such as their
conformance with their specifications) we can design the language with
a massively extensible syntax.
We will first illustrate the current state of art with the programming
language CL designed and implemented in Bratislava. The
formal theory of CL is the simplest of formal theories:
Peano Arithmetic (PA). Definitions of functions and predicates
are just formulas of PA which conservatively extend PA by definitions.
Although a first-order language, CL is not a toy language
because it has been used for six years now in the undergraduate
teaching at the University of Bratislava. Up to 300 students pass
yearly through the four courses based on CL.
CL has a wide set of pattern matching constructs which go far
beyond the ones known from the functional programming languages. The
advantage of pattern matching over the traditional case (if-then-else)
constructs lies in the vastly increased readability of programs. In
addition, the programs obtain a mathematical look and feel. We will
illustrate this point with a brief demo of CL during the
talk. The current implementation of CL has a fixed set of
pattern matching constructs (we call them discriminators ).
The main topic of the talk is a proposal of how to make pattern
matching extensible. User-defined discriminators must be proved
correct in PA before they can be used in definitions of functions and
predicates. Since discriminators can be conditional (the ones
implemented in the current CL are unconditional), they may be
used in definitions only when their conditions are met. This must be
again demonstrated by a proof (by so-called proof obligations).
Participant: David Wahlstedt
If you have any further questions, please mail bove@cs.chalmers.se.
Page last modified on November 12, 2002 by Ana Bove.
Talk: Generalized General Recursion
Abstract:
Talk: Type-based Termination of Recursive Definitions ---
The Calculus of Constructions
Abstract:
Talk: Proving Termination by Update-induction
Abstract:
Talk: Type-theoretic Functional Semantics
Abstract:
Talk: Type Theory and Rewriting
Abstract:
Talk: Modelling General Recursion in Type Theory
Abstract:
Talk: General Recursion via Coinductive Types
Abstract:
Talk: A Unifying Approach to Recursive and Co-recursive Definitions
Abstract:
Talk: Size-change Termination Principle in Partial Evaluation
Abstract:
Talk: Normalization for eta-Expansion in Pure Type Systems
Abstract:
Talk: Strong Normalization for Nested (Co-)Recursion
Abstract:
Talk: Seeing and Doing
Abstract:
Talk: Views for Recursion
Abstract:
Talk: Recursion Schemes from Comonads a la Mendler
Abstract:
Talk: What Do We Gain by Integrating a Programming Language with a
Theorem Prover?
Abstract:
Talk: A Small Language with Dependent Types, General Recursion and
Size-change Termination
Abstract: