# Publications on Lambda calculus

## 2017

- Clocked Lambda CalculusJörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew PolonskyMathematical Structures in Computer Science , 27 (5) , pp. 782–806 (2017)paper
# Summary

We introduce the

*clocked lambda calculus*, an extension of the classical lambda calculus with a unary symbol \( \tau \) that serves as a witness of \( \beta \)-steps. This calculus consists of the following two rules: \[ \begin{aligned} (\lambda x.M) N &\to \tau( M[x = N] ) \\ \tau(M)N &\to \tau(MN) \end{aligned} \] The clocked lambda-calculus is infinitary strongly normalizing, infinitary confluent, and the unique infinitary normal forms constitute enriched Böhm trees (more precisely, Lévy-Longo trees), which we call*clocked Böhm trees*. We show that clocked Böhm trees are suitable for discriminating a rich class of lambda terms having the same Böhm trees.See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

# Bibtex

@article{clocked:lambda:calculus:2017, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew}, title = {{Clocked Lambda Calculus}}, journal = {Mathematical Structures in Computer Science}, volume = {27}, number = {5}, pages = {782--806}, year = {2017}, doi = {10.1017/S0960129515000389}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.1017/S0960129515000389

## 2014

- Discriminating Lambda-Terms Using Clocked Boehm TreesJörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew PolonskyLogical Methods in Computer Science , 10 (2) (2014)paper
# Summary

As observed by Intrigila, there are hardly techniques available in the lambda calculus to prove that two lambda terms are not \( \beta \)-convertible. Techniques employing the usual Böhm trees are inadequate when we deal with terms having the same Böhm tree. This is the case in particular for fixed-point combinators, as they all have the same Böhm tree.

Another interesting equation, whose consideration was suggested by Scott, is BY = BYS, an equation valid in the classical model \( P \omega \) of lambda calculus, and hence valid with respect to Böhm tree-equality, but nevertheless the terms are \( \beta \)-inconvertible.

To prove such beta-inconvertibilities, we refine the concept of Böhm trees: we introduce

*clocked Böhm trees's*with annotations that convey information of the tempo in which the Böhm trees are produced. Böhm trees are thus enriched with an intrinsic clock behaviour, leading to a refined discrimination method for lambda terms. An analogous approach pertains to Levy-Longo trees and Berarducci trees.We illustrate applicability of our refined Böhm trees at the following examples:

- We show how to \( \beta \)-discriminate a large number of fixed-point combinators.
- We answer a question of Gordon Plotkin:
*Is there a fixed point combinator \( Y \) such that \[ Y ( \lambda z. f zz ) =_\beta Y ( \lambda x. Y ( \lambda y. f xy )) \]*

*atomic clocks*.This paper is an extended version of

*Modular Construction of Fixed Point Combinators and Clocked Böhm Trees*(LICS 2010).See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

# Bibtex

@article{lambda:clocks:2014, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew}, title = {{Discriminating Lambda-Terms Using Clocked Boehm Trees}}, journal = {Logical Methods in Computer Science}, volume = {10}, number = {2}, year = {2014}, doi = {10.2168/LMCS-10(2:4)2014}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.2168/LMCS-10(2:4)2014

- Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and CounterexamplesJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van OostromLogical Methods in Computer Science , 10 (2:7) , pp. 1–33 (2014)paper
# Bibtex

@article{infinitary:weakly:orthogonal:2014, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van~Oostrom, Vincent}, title = {{Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples}}, journal = {Logical Methods in Computer Science}, volume = {10}, number = {2:7}, pages = {1--33}, year = {2014}, doi = {10.2168/LMCS-10(2:7)2014}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.2168/LMCS-10(2:7)2014

## 2013

- Clocks for Functional ProgramsJörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew PolonskyIn: The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday, pp. 97–126, Springer (2013)paper
# Summary

The contribution of this paper is twofold.

First, we derive a complete characterization of all

*simply-typed***fixed-point combinator (fpc) generators**using*Barendregt's Inhabitation Machines*. A fpc generator is a lambda term \( G \) such that \( Y G \) is a fpc whenever \( Y \) is. The term \( \delta = \lambda xy. y(xy) \), also known as Smullyan's Owl, is a famous fpc generator. For instance, Turing's fpc \( Y_1 \) can be obtaind from Curry's fpc \( Y_0 \) by postfixing \( \delta \): \[ Y_1 = Y_0 \delta \]Second, we present a conjecture that vastly generalises Richard Statman's question on the existance of double fixed-point combinators. Statman asked whether there is a fixed-point combinator \( Y \) such that \( Y =_\beta Y \delta \). This question remains open as the proof by Benedetto Intrigila contains a gap. We have the following conjecture about the relation of the \( \mu \)-opertator and fixed-point combinators:

ConjectureWe conjecture that for any fixed-point combinator \( Y \) and simply-typed \( \lambda\mu \)-terms \( s,t \) it holds that \[ s =_{ \beta \mu } t \iff s_Y =_{ \beta } t_Y \] where \(s_Y, t_Y\) are the*untyped*lambda terms obtained from \(s,t\), respectively, by replacing all occurrences of \( \mu \)-operators with the fixed-point combinator \( Y \).See research for an overview of my research on the clocked lambda claculus and fixed-point combinators.

# Bibtex

@inproceedings{lambda:clocks:functional:programs:2013, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem and Polonsky, Andrew}, title = {{Clocks for Functional Programs}}, booktitle = {The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday}, pages = {97--126}, year = {2013}, doi = {10.1007/978-3-642-40355-2\_8}, series = {LNCS}, volume = {8106}, publisher = {Springer}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.1007/978-3-642-40355-2_8

## 2012

- Highlights in Infinitary Rewriting and Lambda CalculusJörg Endrullis, Dimitri Hendriks, and Jan Willem KlopTheoretical Computer Science , 464 , pp. 48–71 (2012)paper
# Bibtex

@article{infinitary:highlights:2012, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem}, title = {{Highlights in Infinitary Rewriting and Lambda Calculus}}, journal = {Theoretical Computer Science}, volume = {464}, pages = {48--71}, year = {2012}, doi = {10.1016/j.tcs.2012.08.018}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {journal} }

# Digital Object Identifier

10.1016/j.tcs.2012.08.018

## 2010

- Modular Construction of Fixed Point Combinators and Clocked Böhm TreesJörg Endrullis, Dimitri Hendriks, and Jan Willem KlopIn: Proc. Symp. on Logic in Computer Science (LICS 2010), pp. 111–119, IEEE Computer Society (2010)paper
# Summary

One of the best-known methods for discriminating lambda terms with respect to \( \beta \)-convertibility is due to Corrado Böhm. Roughly speaking, the

*Böhm tree*of a lambda term is its infinite normal form. If lambda terms have distinct Böhm trees, then they are not \( \beta \)-convertible. But what if their Böhm trees coincide? For example, all fixed-point combinators have the same Böhm tree, namely \[ \lambda x. x(x(x(\ldots))) \]We refine Böhm trees with a

*clock*that records how many head reduction steps have been used to rewrite each subterm to head normal form. We show that*clocked Böhm trees*are suitable for discriminating a rich class of lambda terms (in particular many fixed-point combinators) having the same Böhm trees.We refer to

*Discriminating Lambda-Terms Using Clocked Boehm Trees*(LMCS 2014) for an extended journal version of this paper. In the extended version we improve the precision of the clocks to*atomic clocks*and we answer a question of Gordon Plotkin, showing that the method can be used beyond simple terms.# Bibtex

@inproceedings{lambda:clocks:2010, author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem}, title = {{Modular Construction of Fixed Point Combinators and Clocked B\"{o}hm Trees}}, booktitle = {Proc.\ Symp.\ on Logic in Computer Science (LICS~2010)}, pages = {111--119}, publisher = {{IEEE} Computer Society}, year = {2010}, doi = {10.1109/LICS.2010.8}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {conference} }

# Digital Object Identifier

10.1109/LICS.2010.8

- Unique Normal Forms in Infinitary Weakly Orthogonal RewritingJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van OostromIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2010), pp. 85–102, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)paper
# Bibtex

@inproceedings{infinitary:weakly:orthogonal:unique:normal:forms:2010, author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri and Klop, Jan Willem and van~Oostrom, Vincent}, title = {{Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2010)}, volume = {6}, pages = {85--102}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, series = {LIPIcs}, year = {2010}, doi = {10.4230/LIPIcs.RTA.2010.85}, keywords = {rewriting, infinitary rewriting, lambda calculus}, type = {conference} }

# Digital Object Identifier

10.4230/LIPIcs.RTA.2010.85

## 2008

- Reduction under SubstitutionJörg Endrullis, and Roel C. de VrijerIn: Proc. Conf. on Rewriting Techniques and Applications (RTA 2008), pp. 425–440, Springer (2008)paper
# Bibtex

@inproceedings{lambda:reduction:under:substitution:2008, author = {Endrullis, J\"{o}rg and de~Vrijer, Roel C.}, title = {{Reduction under Substitution}}, booktitle = {Proc.\ Conf.\ on Rewriting Techniques and Applications (RTA~2008)}, volume = {5117}, pages = {425--440}, publisher = {Springer}, series = {LNCS}, year = {2008}, doi = {10.1007/978-3-540-70590-1\_29}, keywords = {rewriting, lambda calculus}, type = {conference} }

# Digital Object Identifier

10.1007/978-3-540-70590-1_29