|
Published
- Felix Joachimski and Ralph Matthes
Short Proofs of Normalization for the simply-typed lambda-calculus,
permutative conversions and Gödel's T
Archive for Mathematical Logic 42:59-87, 2003.
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 generalized
elimination rules in natural deduction, advocated by von Plato, 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.
- Felix Joachimski and Ralph Matthes
Standardization and confluence for a lambda calculus with generalized
applications.
In Leo Bachmair (Editor), Proceedings of 11th RTA 2000 (Norwich), Lecture Notes in Computer Science 1833, pp.
141-155, Springer-Verlag 2000.
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.
- Klaus Aehlig and Felix Joachimski
On Continuous Normalization
ps ps.gz ps.gz (2pps) pdf.gz bib-entry Haskell Parser Examples
In Julian Bradfield (Editor), Proceedings of CSL’02 (Edinburgh), Lecture Notes in Computer Science 2471, pp. 59-73, Springer-Verlag 2002.
This work aims at explaining the syntactical properties of continuous normalization, as introduced in proof theory by Mints, and
further studied by Ruckert, Buchholz and Schwichtenberg.
In an extension of the untyped coinductive lambda-calculus by void constructors (so-called repetition rules), a primitive recursive normalization
function is defined. Compared with other formulations of continuous normalization, this definition is much simpler and therefore suitable for analysis in a coalgebraic setting. It is shown to be continuous
w.r.t. the natural topology on non-wellfounded terms with the identity as modulus of continuity.
The number of repetition rules is locally related to the number of beta-reductions necessary to reach the
normal form (as represented by the Böhm tree) and the number of applications appearing in this normal form.
- Felix Joachimski
Confluence of the Coinductive Lambda-Calculus
ps ps.gz ps.gz (2pps) pdf.gz bib-entry
September 2001, accepted by TCS, revised 12/2002, 4/2003.
The coinductive lambda-calculus Lambda^\co
arises by a coinductive interpretation of the grammar of the standard lambda-calculus Lambda and contains non-wellfounded lambda-terms. An appropriate notion of reduction is analyzed and proven to be confluent
by means of a detailed analysis of the usual Tait/Martin-Löf style development argument. This yields bounds for the lengths of those joining reduction sequences that are guaranteed to exist by confluence. These
bounds also apply to the wellfounded lambda-calculus, thus adding quantitative information to the classic result.
- Klaus Aehlig and Felix Joachimski
Operational Aspects of Normalization by Evaluation
ps ps.gz ps.gz (2pps) pdf.gz bib-entry Haskell Examples
October 2001, accepted by MSCS, revised 5/2002, 4/2004.
A purely syntactic and untyped variant of
Normalization by Evaluation for the lambda-calculus is presented in the framework of a two-level lambda-calculus with rewrite rules to model the inverse of the evaluation functional. Among its operational
properties figures a standardization theorem that formally establishes adequacy of implementation in functional programming languages. An example implementation in Haskell is provided. The relation to usual
type-directed Normalization by Evaluation is highlighted, using a short analysis of eta-expansion that leads to a perspicuous strong normalization and confluence proof for beta-eexp-reduction as a byproduct.
- Felix Joachimski
Syntactic Analysis of eta-Expansions in Pure Type Systems
ps ps.gz ps.gz (2pps) pdf.gz bib-entry
Information and Computation, 182(1):53-71 (2003).
By a detailed analysis of the interaction between
beta-reduction and eta-expansion in the simply typed lambda-calculus, a modular and purely syntactic proof method is devised in order to derive strong normalization of the combined reduction from that of beta
and eta-expansion. It is shown how this technique extends to beta-normalizing functional Pure Type Systems with Barthe's formulation of eta-expansion.
Unpublished
- Felix Joachimski
Standardization for the Coinductive Lambda-Calculus
ps ps.gz ps.gz (2pps) pdf.gz bib-entry
February 2002.
In the calculus Lambda^co of possibly non-wellfounded
lambda-terms, standardization is proved for a parallel notion of reduction. For this system confluence has recently been established by means of a bounding argument for the number of reductions provoked by the
joining function which witnesses the confluence statement.
Similarly, bounds have to be introduced in order to turn the proof of standardization for the wellfounded lambda-calculus into a sound coinductive
argument, thus limiting the number of reduction steps arising in the process of standardization. This leads to elementary complexity bounds for the length of the resulting standard reduction sequence in terms of
the length of the input sequence. A fortiori, these bounds also apply to the usual wellfounded lambda-calculus, strengthening previous results by Xi.
- Klaus Aehlig and Felix Joachimski
Continuous Normalization for the Untyped Lambda-Calculus and Gödel’s T
ps ps.gz ps.gz (2pps) pdf.gz pdf bib-entry
January 2003, submitted to APAL.
Building on previous work by Mints,
Buchholz and Schwichtenberg, a simplified version of continuous normalization for the untyped lambda-calculus and Gödel's T is presented and analyzed in the coalgebraic framework of non-wellfounded terms with
so-called repetition constructors.
The primitive recursive normalization function is uniformly continuous w.r.t. the natural metric on non-wellfounded terms. Furthermore, the number of necessary repetition
constructors is locally related to the number of reduction steps needed to reach and the size of the normal form (as represented by the Böhm tree).
It is also shown how continuous normal forms relate to
derivations of strong normalizability in the typed lambda-calculus and how this leads to new bounds for the sum of the height of the reduction tree and the size of the normal form.
Finally, the methods are
extended to an infinitary lambda-calculus with omega-rule and permutative conversions and this is used to derive a strong form of normalization for an iterative version of Gödel's system T, leading to a value
table semantics for number-theoretic functions.
- Felix Joachimski
On Zucker’s isomorphism for LJ and its extension to Pure Type Systems
Submitted to JFP, March 2003.
ps ps.gz ps.gz (2pps) pdf.gz pdf bib-entry
It is shown how the sequent calculus LJ can be embedded into a simple
extension of the lambda-calculus by generalized applications, called LambdaJ. The reduction rules of cut elimination and normalization can be precisely correlated, if explicit substitutions are added to LambdaJ.
The resulting system LambdaJ_s is proved strongly normalizing, thus showing strong normalization for Gentzen's cut elimination steps. This refines previous results by Zucker, Pottinger and Herbelin on the
isomorphism between natural deduction and sequent calculus.
The concept of generalized applications extends to Pure Type Systems, so that in particular sequent calculus analogues for all systems of the
lambda-cube arise. Cut-elimination and strong beta-normalization are shown to be equivalent for all Pure Type Systems.
Miscellanous
- The final version of my doctoral thesis:
Reduction properties of PIE-Systems
ps ps.gz ps.gz (2pps) pdf.gz bib-entry
This is the version that was printed. The thesis has been submitted on
November 13 2001 and underwent some minor revisions since then.
I am most appreciative for any comment, remark, references, counter examples. Of course, I am sorry for all the errors that occur in this work
(and for the sheer volume of it)
- My master’s thesis (german)
Kontrolloperatoren und klassische Logik
1996. Supervisor: Prof. Helmut Schwichtenberg.
|
