 |
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
-
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.
-
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
-
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.
-
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.
-
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
-
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.
-
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.
-
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
-
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.
-
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).
-
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
|
|
