In this paper we revisit an unpublished but influential technical report from 1978 by N.G. de Bruijn, written in the framework of the Automath project. This report describes a technique for proving confluence of abstract reduction systems, called the weak diamond property. It paved the way for the powerful technique developed by Van Oostrom to prove confluence of abstract reduction systems, called decreasing diagrams.
We first revisit in detail De Bruijn’s old proof, providing a few corrections and hints for understanding. We find that this original criterion and proof technique are still worthwhile. Next, we establish that De Bruijn’s confluence criterion can be used to derive the decreasing diagrams theorem (the reverse was already known). We also provide a short proof of decreasing diagrams in the spirit of De Bruijn. We finally address the issue of completeness of this method.
See research for an overview of my research on confluence.
Bibtex
@article{confluence:weak:diamond:2013,
author = {Endrullis, J\"{o}rg and Klop, Jan Willem},
title = {{De Bruijn’s Weak Diamond Property Revisited}},
journal = {Indagationes Mathematicae},
volume = {24},
number = {4},
pages = {1050 -- 1072},
year = {2013},
doi = {10.1016/j.indag.2013.08.005},
note = {In memory of N.G. (Dick) de Bruijn (1918–2012)},
keywords = {rewriting, confluence},
type = {journal}
}
@inproceedings{termination:sat:compilation:2014,
author = {Bau, Alexander and Endrullis, J\"{o}rg and Waldmann, Johannes},
title = {{SAT compilation for Termination Proofs via Semantic Labelling}},
booktitle = {Proc.\ Workshop on Termination (WST~2007)},
year = {2013},
keywords = {rewriting, termination},
type = {workshop}
}
Digital Object Identifier
Clocks for Functional Programs
Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky
In: The Beauty of Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday, pp. 97–126, Springer (2013)
First, we derive a complete characterization of all simply-typedfixed-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:
Conjecture
We 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 \).
This conjecture immediately implies a negative answer to Statman's question.
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}
}
@article{streams:forever:2013,
author = {Endrullis, J\"{o}rg and Hendriks, Dimitri and Klop, Jan Willem},
title = {{Streams are Forever}},
journal = {Bulletin of the {EATCS}},
volume = {109},
pages = {70--106},
year = {2013},
keywords = {streams, degrees, automata},
type = {journal}
}
Digital Object Identifier
Mix-Automatic Sequences
Jörg Endrullis, Clemens Grabmayer, and Dimitri Hendriks
In: Proc. Conf. on Language and Automata Theory and Applications (LATA 2013), pp. 262–274, Springer (2013)
@inproceedings{streams:mix:automatic:2013,
author = {Endrullis, J\"{o}rg and Grabmayer, Clemens and Hendriks, Dimitri},
title = {{Mix-Automatic Sequences}},
booktitle = {Proc.\ Conf.\ on Language and Automata Theory and Applications (LATA~2013)},
volume = {7810},
pages = {262--274},
publisher = {Springer},
series = {LNCS},
year = {2013},
doi = {10.1007/978-3-642-37064-9\_24},
keywords = {streams, automata},
type = {conference}
}