computer science

	STAFF — Fer-Jan de Vries   Dr (Universiteit Utrecht) Lecturer
	F32 Computer Science Building Department of Computer Science, University of Leicester, University Road, Leicester, LE1 7RH. T: +44 (0) 116 252 3903 E: fdv1 at mcs le ac uk

A selected annotated bibliography

1. J.R. Kennaway and F.J. de Vries. Infinitary Rewriting. Chapter 12 in Terese, editor, Term Rewriting Systems (Cambridge Tracts in Theoretical Computer Science 55), Cambridge University Press. Page 668-711. 2003.

   In this chapter we develop a general theory of infinite orthogonal rewriting unifying our earlier work on infinite term rewriting and infinite lambda calculus. Confluence in the infinitary setting is significantly harder than in the finitary case. The technique of transfinite tiling diagrams in the confluence proof is new. Infinitary extensions of confluent finite systems may not be confluent, unless one adds a rule that identifies "meaningless" terms by reducing them to bottom. Then the extensions become confluent and normalising; the sets of their normal forms can give new denotational semantics of the original finite systems.

2. P. Severi and F.J. de Vries. An Extensional Böhm Model. Conference paper in Sophie Tison, editor, Rewiting Techniques and Applications, Proceedings of the 13th International Conference, RTA 2002, Copenhagen Denmark, July 2002. (Lecture Notes in Computer Science 2378), Springer-Verlag. Page 159-173. 2002.

   Here we present the first confluent and normalising infinitary extension of extensional lambda calculus using transfinite tiling diagrams from [Kennaway-de Vries 2003]. This requires new infinitary commutation and postponement results for eta reduction and beta-bottom reduction. Application: the set of normal forms of the extension is a simple (i.e.,\ not using Barendregt's continuity techniques) description of Barendregt and Dezani's extensional eta-Böhm tree model and gives us a simple and direct (no detour via a D-infinity semantics!) syntax-based proof that two lambda terms are equal in this model if and only if they are observationally equivalent wrt to eta-beta normal forms.

3. S. van Bakel, F. Barbanera, M. Dezani-Ciancaglini, F.J. de Vries. Intersection Types for Lambda Trees. Theoretical Computer Science 272(1-2): 3-40, 2002.

   Trees have been used to give syntax-flavoured semantics to lambda calculus. As such they play an important role in the understanding of lambda calculus. In this paper we study five families of trees and we present an intersection type assignment system parametric with respect to these five families. Then we prove, in an (almost) uniform way, that each type assignment system fully describes the observational equivalence induced by the corresponding tree representation of lambda terms. For two families of extensional trees this gives new results and, for the other families of trees, this unifies and improves earlier results.

4. M. Dezani-Ciancaglini, P. Severi and F.J. de Vries. Infinitary Lambda Calculus and Discrimination of Berarducci trees. Theoretical Computer Science 298(2):275 - 302, 2003.

   Tree semantics of lambda calculus induce equality relations on lambda terms. For the common tree semantics various authors have given alternative characterisations in the form of observational equivalence of suitable extensions of lambda calculus. Berarducci trees are a recent tree semantics. The induced equality relation is included in all equality relations induced by a tree semantics. In this paper we give such a characterisation for Berarducci trees. To do so we make an essential use of our recently developed techniques for infinite rewriting.

5. P. Severi and F.J. de Vries. Continuity and Discontinuity in Lambda Calculus. Conference paper in Pawel Urzyczyn, editor, Typed Lambda Calculus and Applications, Proceedings of the 7th International Conference, TLCA 2005, Nara Japan, April 21-23 2005. (Lecture Notes in Computer Science 3461), Springer-Verlag. Page 369-385. 2005.

   In [Kennaway-de Vries 2003] we presented a general construction of tree semantics from a set of "meaningless" terms. Properties of these semantics have not been studied before. Observing that Barendregt's Böhm model construction for lambda calculus depends heavily on continuity, in contrast to our general construction, and that the Berarducci model is not continuous, it is a natural question to ask when a tree model of the lambda calculus is continuous. We prove that the only continuous trees semantics are the Böhm and the Levy-Longo model and that only these two models have an approximation theorem and continuous context operators.

6. P. Severi and F.J. de Vries. Order Structures on Böhm-like Models. Conference paper in Luke Ong, editor, Computer Science Logic: 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK. August 22-25, 2005. (Lecture Notes in Computer Science 3634), Springer-Verlag. Page 103-116. 2005.

   In [Kennaway-de Vries 2003] we presented a general construction of tree semantics for lambda calculus parametrised by a set of "meaningless" terms. Here we give many new examples of meaningless sets. We study whether the resulting tree semantics are orderable. The six principal models (including the Böhm and the Lévy-Longo model) are orderable by the prefix relation. The Berarducci model is also orderable. However, orderability is not the norm. We give a syntactic proof that at least 2^c such tree semantics are unorderable, where c is the cardinality of the continuum. Salibra's Theorem is a corollary.

7. J.R. Kennaway, M.R. Sleep P. Severi and F.J. de Vries.
   Infinite rewriting: from syntax to semantics, in proceedings of Processes, Terms and Cycles: Steps on the Road to Infinity: Essays dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, editors: A. Middeldorp, V. van Oostrom, F. van Raamsdonk and R. de Vrijer. SLNCS 3838, pages 148-172, 2005. pdf

   Part one of this paper is a brief summary of the theory of infinitary rewriting; part two presents as application recent work presented at CSL05 and TLCA05 plus some new results by Severi and de Vries on the lattice of tree semantics for lambda calculus. Each tree semantics consist of the set of normal forms of a confluent and normalising infinitary extension of lambda calculus build from a set of "meaningless" terms. Using their syntactic descriptions these sets of meaningless terms can be ordered into a rich lattice, providing some insight in the even richer lattice of lambda models.

• Research
• Interests
• Publications
• Brief CV

• Teaching
• Courses

• MPhil/PhD matters
• PhD Tutor
• Current Students
• Expected students
• PhD Admissions
• Graduate Studies Committee
• Overview

• Student Support and Welfare
• Student Support and Welfare Page
• Welfare Tutor Page

Author: Fer-Jan de Vries   Dr (Universiteit Utrecht) (fdv1 at mcs le ac uk), T: +44 (0) 116 252 3903.
© University of Leicester 16 September, 2000 . Last modified: 2nd November 2011, 15:34:11.
CS Web Maintainer. Any opinions expressed on this page are those of the author.