The Coq mailing list

[peio borthelle <pborthelle AT hadoly.fr>]

Hi Helmut,

I must admit I did not read your paper very thoroughly but on first 
impression it seems like a fun construction!

A couple remarks/pointers into the literature.

I believe that what you call "universal lambda term" is commonly 
referred to as a "meta-circular evaluator". Very similar construction 
are quite common in the lisp tradition (which arguably are the concrete 
languages closest in spirit to pure untyped lambda calculus). See for 
example section 4.1 "The Metacircular Evaluator" from the wizard book 
[1]. The concept of "definitional interpreter" by John Reynolds is also 
quite close to this idea too, you might be interested in reading [2].

Note that traditional meta-circular evaluators typically use an 
environment instead of substitution as you did, but indeed numerous 
variations exist (in implementation style, reduction strategy or source 
term encoding).

Also, while the goal and result are completely different than what you 
do, this quest for some kind of universal term in lambda calculus makes 
me think of "universal combinators", a single function which is 
sufficient to express all the others (using composition). This idea was 
surveyed by Jeroen Fokker [3] and has been explored in a funny little 
esoteric programming language by Chris Barker [4].

Best,
Peio

[1] https://web.mit.edu/6.001/6.037/sicp.pdf
[2] https://dl.acm.org/doi/10.1145/800194.805852
[3] https://dl.acm.org/doi/10.1007/BF03180572
[4] https://esolangs.org/wiki/Iota