University of Leicester

cms

photo of Fer-Jan de Vries 		 	 Dr (Universiteit Utrecht)

STAFF — Fer-Jan de Vries   Dr (Universiteit Utrecht)

Former Lecturer
Ken Edwards Building
School of Computing and Mathematical Sciences,
University of Leicester,
University Road,
Leicester,
LE1 7RH.

E: fer.jan.de.vries at gmail.com







Research

Infinite computations are a main current theme of my interests in the theory and semantics of computation, language and logic.

Recent publications until June 2021

  1. Many-valued logics inside lambda-calculus
    in Logical Methods in Computer Science, volume 17(2), paper 25, pages 1-16, 29 June, 2021.
    pdf, URL: arXiv:1810.07667
    Abstract We will extend the well-known Church encoding of Boolean Logic in $\lambda$-calculus to an encoding of McCarthy's $3$-valued logic into a suitable infinitary extension of $\lambda$-calculus that identifies all unsolvables by $\bot$, where $\bot$ is a fresh constant. This encoding refines to $n$-valued logic for $n \in \{4,5\}$. Such encodings also exist for Church's original $\lambda I$-calculus.
    By way of motivation we consider Russell's paradox, exploiting the fact that the same encoding allows us also to calculate truth values of infinite closed propositions in this infinitary setting.
  2. P. Severi and F.J. de Vries.
    The Infinitary Lambda Calculus of the Infinite Eta Bohm Trees
    in Mathematical Structures in Computer Science (June 2017): Computing with lambda-terms: A special issue dedicated to Corrado Böhm for his 90th birthday
    pdf, DOI: http://dx.doi.org/10.1017/S096012951500033X

    Abstract In this paper we introduce a strong form of eta reduction called etabang that we use to construct a confluent and normalising infinitary lambda calculus, of which the normal forms correspond to Barendregt’s infinite eta Bohm trees. This new infinitary perspective on the set of infinite eta Bohm trees allows us to prove that the set of infinite eta B ̈hm trees is a model of the lambda calculus. The model is of interest because it has the same local structure as Scott’s D-infinity-models, i.e. two finite lambda terms are equal in the infinite eta B ̈hm model if and only if they have the same interpretation in Scott’s D-infinity-models
  3. F.J. de Vries.
    On Undefined and Meaningless in Lambda Definability
    in proceedings of 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    pdf, DOI: 10.4230/LIPIcs.FSCD.2016.18, URL: http://drops.dagstuhl.de/opus/volltexte/2016/5978/

    Abstract We distinguish between undefined terms as used in lambda definability of partial recursive functions and meaningless terms as used in infinite lambda calculus for the infinitary terms models that generalise the Bohm model. While there are uncountable many known sets of meaningless terms, there are four known sets of undefined terms. Two of these four are sets of meaningless terms. In this paper we first present set of sufficient conditions for a set of lambda terms to serve as set of undefined terms in lambda definability of partial functions. The four known sets of undefined terms satisfy these conditions. Next we locate the smallest set of meaningless terms satisfying these conditions. This set sits very low in the lattice of all sets of meaningless terms. Any larger set of meaningless terms than this smallest set is a set of undefined terms. Thus we find uncountably many new sets of undefined terms. As an unexpected bonus of our careful analysis of lambda definability we obtain a natural modification, strict lambda-definability, which allows for a Barendregt style of proof in which the representation of composition is truly the composition of representations.
  4. A. Kurz, A. Pardo, D. Petrisan, P. Severi and F.J. de Vries.
    Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes
    in proceedings of 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)
    pdf, DOI: 10.4230/LIPIcs.CALCO.2015.205, URL: http://drops.dagstuhl.de/opus/volltexte/2015/5535/

    Abstract The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible non- termination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekič lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types.
  5. P. Severi and F.J. de Vries.
    The Infinitary Lambda Calculus of the Infinite Eta Bohm Trees
    in Mathematical Structures in Computer Science (FirstView Article: 17 August 2015): Computing with lambda-terms: A special issue dedicated to Corrado Böhm for his 90th birthday
    pdf DOI: http://dx.doi.org/10.1017/S096012951500033X

    Abstract In this paper we introduce a strong form of eta reduction called etabang that we use to construct a confluent and normalising infinitary lambda calculus, of which the normal forms correspond to Barendregt’s infinite eta Bohm trees. This new infinitary perspective on the set of infinite eta Bohm trees allows us to prove that the set of infinite eta B ̈hm trees is a model of the lambda calculus. The model is of interest because it has the same local structure as Scott’s D-infinity-models, i.e. two finite lambda terms are equal in the infinite eta B ̈hm model if and only if they have the same interpretation in Scott’s D-infinity-models
  6. A. Kurz, D. Petrisan, P. Severi and F.J. de Vries.
    Nominal Coalgebraic Data Types with Applications to Lambda Calculus
    in LMCS 2013, volume 9(4), paper 20, pages 1-52, 2013.
    pdf

    Abstract We investigate final coalgebras in nominal sets. This allows us to define types of infinite data with binding for which all constructions automatically respect alpha equivalence. We give applications to the infinitary lambda calculus.
  7. P. Severi and F.J. de Vries.
    Completeness of Conversion between Reactive Programs for Ultrametric Models
    in Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. SLNCS volume 7941, pages 221-235, 2013. .
    pdf

    Abstract In 1970 Friedman proved completeness of beta eta conversion in the simply-typed lambda calculus for the set-theoretical model. Re- cently Krishnaswami and Benton have captured the essence of Hudak’s reactive programs in an extension of simply typed lambda calculus with causal streams and a temporal modality and provided this typed lambda calculus for reactive programs with a sound ultrametric semantics. We show that beta eta conversion in the typed lambda calculus of reac- tive programs is complete for the ultrametric model.
  8. P. Severi and F.J. de Vries.
    Pure Type Systems with Corecursion on Streams
    in Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012.
    pdf

    Abstract In this paper, we use types for ensuring that programs involving streams are well-behaved. We extend pure type systems with a type constructor for streams, a modal operator next and a fixed point operator for expressing corecursion. This extension is called Pure Type Systems with Corecursion (CoPTS). The typed lambda calcu- lus for reactive programs defined by Krishnaswami and Benton can be obtained as a CoPTS. CoPTS’s allow us to study a wide range of typed lambda calculi extended with corecursion using only one framework. In particular, we study this extension for the calculus of constructions which is the underlying formal language of Coq. We use the machinery of infinitary rewriting and formalize the idea of well-behaved programs using the concept of infinitary normalization. We study the properties of infinitary weak and strong normalization for CoPTS’s. The set of finite and infinite terms is defined as a metric completion. We shed new light on the meaning of the modal operator by connecting the modality with the depth used to define the metric. This connection is the key to the proofs of infinitary weak and strong normalization
  9. P. Severi and F.J. de Vries.
    Meaningless Sets in Infinitary Combinatory Logic
    in proceedings of RTA 2012, the 23rd International Conference on Rewriting Techniques and Applications. Editor Ashish Tiwari. Nagoya, May 28 -June 2, 2012. Leibniz International Proceedings in Informatics (LIPIcs) volume 15. Pages 288--304.
    pdf

    Abstract In this paper we study meaningless sets in infinitary combinatory logic. So far only a handful of meaningless sets were known. We show that there are uncountably many meaningless sets. As an application to the semantics of finite combinatory logics, we show that there exist uncountably many combinatory algebras that are not a lambda algebra. We also study ways of weakening the axioms of meaningless sets to get, not only sufficient, but also necessary conditions for having confluence and normalisation.
  10. A. Kurz, D. Petrisan, P. Severi and F.J. de Vries.
    An Alpha-Corecursion Principle for the Infinitary Lambda Calculus
    in postproceedings of CMCS 2012: the 11th International Workshop on Coalgebraic Methods in Computer Science. 31 March - 1 April 2012, Tallinn, Estonia. SLNCS volume 7399, pages 130-149, 2012.
    pdf

    Abstract Gabbay and Pitts proved that lambda-terms up to alpha-equivalence constitute an initial algebra for a certain endofunctor on the category of nominal sets. We show that the terms of the infinitary lambda-calculus form the final coalgebra for the same functor. This allows us to give a corecursion principle for alpha-equivalence classes of finite and infinite terms. As an application, we give corecursive definitions of substitution and of infinite normal forms (Bohm, Levy-Longo and Berarducci trees).
  11. P. Severi and F.J. de Vries.
    Weakening the Axiom of Overlap in Infinitary Lambda Calculus
    in proceedings of RTA2011: the 22nd International Conference on Rewriting Techniques and Applications. Editor Manfred Schmidt-Schauß. Novi Sad. May 30 - June 1, 2011. Leibniz International Proceedings in Informatics (LIPIcs) volume 10. Pages 313--328.
    pdf

    Abstract In this paper we present a set of necessary and sufficient conditions on a set of lambda terms to serve as the set of meaningless terms in an infinitary bottom extension of lambda calculus. So far only a set of sufficient conditions was known for choosing a suitable set of meaningless terms to make this construction produce confluent extensions. The conditions covered the three main known examples of sets of meaningless terms. However, the much later construction of many more examples of sets of meaningless terms satisfying the sufficient conditions renewed the interest in the necessity question and led us to reconsider the old conditions. The key idea in this paper is an alternative solution for solving the overlap between beta reduction and bottom reduction. This allows us to reformulate the Axiom of Overlap, which now determines together with the other conditions a larger class of sets of meaningless terms. We show that the reformulated conditions are not only sufficient but also necessary for obtaining a confluent and normalizing infinitary lambda beta bottom calculus. As an interesting consequence of the necessity proof we obtain for infinitary lambda calculus with beta and bot reduction that confluence implies normalization.

My old PhD thesis

Proefschrift






























Author: Fer-Jan de Vries   Dr (Universiteit Utrecht) (fer.jan.de.vries at gmail.com).
© University of Leicester 16 September, 2000 . Last modified: 30th June 2021, 23:30:49
CMS Web Maintainer. Any opinions expressed on this page are those of the author.