coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simulating lambda terms in lambda calculus

From: Helmut Brandl <helmut.brandl AT gmx.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Simulating lambda terms in lambda calculus
Date: Wed, 25 Sep 2024 21:47:43 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
Ironport-data: A9a23:C6SYaKnmhPCvAHA0/EeJ84vo5gyeJ0RdPkR7XQ2eYbSJt1+Wr1Gzt xIXCD/QPvaIN2H3fYpwbI+08BtQ78DcndQ2HAdvrStmQVtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayazp8B56r8ks14Kyj4m5A5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1PD2I5FKI9udxbOm5/6 /giOionQECq0rfeLLKTEoGAh+wmK9T3eowaqjdmwC2x4fQOG8mZBf+QupkBg3Fq3qiiHt6GD yYdQTpiaBHdf1tFIF4RBJYWk+K4wH/yb1W0rXrM9fduuDiOkFYZPL7FMurlKoWxHPlvpFe7n XLX5CemRVILDYnKodaC2jf27gPVpgvwX5tXH7ml/NZxkViLzyoSDgcXXB21u5GEZlWWXtVCN wob/zpoq6UunKC2cuTAs9SDiCbslnYhtxB4SoXWRSnUokYIy251x1ToTwKtrPQjs9IqAzMvx hmPks+B6fmDdlGKYSr1y1tWhWra1espwasqaioUCw0I/7EPZakt2wnXQI8L/LGd17XI9PKZ/ 9xOhCc7l/MVgNJjO2BXO7zYq2rEm6UlhTLZKukasqxJI++5iEOYi1SU1GXm
Ironport-hdrordr: A9a23:FiAeBKkb7T++S/fZVDyr01E0infpDfL03DAbv31ZSRFFG/Fw8P re/sjztCWZtN91YhodcL+7Scq9qB/nlKKdpLNwAV7dZniChILYFu5fBOLZqlWMJ8S9zJ846U 4KScZD4bPLfD9HpPrbpC+lDt0n3N6Ly6ywg/zCpk0dNj2CE5sQiTuQEWygYzRLreR9dOIE/B Hw3KB6mwY=
Ironport-phdr: A9a23:3P1s9hApJycxdJ7DBqi2UyQUJUkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua41ygWRAM6CsKIMotGVmp6jcFRD26rJiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhFiiaxbalsI BmqrQjdudQajIVhJ60s1hbHv3xEdvhZym9vOV+dhRHw6Nuu8pV+6SpQofUh98BBUaX+Yas1S KFTASolPW4o+sDlrAHPQgST6HQSVGUWiQdIDBPe7B7mRJfxszD1ufR71SKHIMD5V7E0WTCl7 6d2VB/ljToMOjAl/G3LjMF7kaRWqw+jqRNi2Y7ZeJ2aO/VjcK3df9wUS2VPUMVfVyJfBY2xd JcPD/MEPepEr4nxu1kDoB2jDgesHuPvzTpIi2f006Ik1+QhFBzG3BA9FN8TqnTbttP1O7oWU euoy6TIzSvMb/dT2Tfg9IjEaAsuoeuWUrJ2bMXRzVIiFwzAjlSfs4DlOS2a1vgUvmWd8uFvW v6hhXQ9pAFtvjig2N0sio/Ri4wby13J6zl1zJs6KNCmS0N2YMCpHZVSui+aNIZ7Qd8uT39mt Ssk1rELvYO2cDQUxJkn2RPSZeCLfYeW7h//V+ucJypzinxieLK6nRmy8E6gx/X5Vsm1zFZGt DRKncTRtnwVzRPc9s2HRuF6/ke71jaDzx7c6vpDIUAwj6XbLZEhwqUqmpoUq0TDESn7k1j1g q+Obkgo5PWk5/r9brn4uJORNZV4hhz8P6g0hMCzHfw0PwwOUmSB+umx0Kfv8VD3TbhFlPE6j KbUvZDcKM8GuKO5BxJV0p0/6xmhFTeozdUYnHgZI19dZB6KiZXiNUvUL/DiF/i/hkyhkDd1y PDCOb3sGpDNLn/ekLf9Z7p95EtcyQUpwdBZ+Z1UFqkNIPP1WkDvqNzVFgE1PxGqz+r9Ftlxy IETVXiSDqKbKq/er0OE6voqI+aWZY8VvDj9K+Ii5/7rlXI5mUESfa2s3ZsKdHC0BO9pI1+Db nrqn9gBFXwHvgU7TO3lklGCVyBcZ2qqU6I6/T40EJimApvbRoCxnLyB2z+2EoBOamBcFl+MC Wvod5mDW/oUdC2SJdZhniUYWrilVo8uzgqjtBT6yrpiNurb4DcUtZPl1Nhv5u3cjws+9TJuD 5fV72bYRGZt22gMWjUe3aZloEU7xE3Q/7J/hql4GNhW+u8BeB0zM5LYh7h6BtT3Rx6HdM2AT lqiatqjEXc3Q85nkIxGWFp0B9j31kOL5CGtGbJAz9RjZbQx+6PYhT3qItpljmzB3+8nhkUnR c1GMSungLR+/k7dHd2BiF2XwoCtc6lUxyvR7CGb12PbvExcVRNsF6/fVHYTYmPZqMS/4E7eH Pe1EbpyCgJa0oaZL7dSLNjgjFFIXvDmbdTTZ2eshyG6Hx+OyrekY4/6PWMQwHaVE1AKxiYU+ 3vOLg0iHmGhrmbZWSRpDk7qaljw/PNWrXSmUgk7yhHMaUB9v1as0jgSg/HUC/Ya37Ze/Twkt y0xBlG2mdTfF9uHoQNlOqRae9I0plldhyrfsERmM5qsIroH5BZWehlrv07oyxR8C5lR2ckso nQwyQNuKKWemFpffjKc1Jr0N/XZMG73tByobqfX3BnZ3rP0su8P5fA9tkmlthugEEYm23piw 59T3mfdrpTGAQwOUI7gB14t/ksyrLXbby8hooLMgCc1a+/u6GCEgo1vXrN2r3ToN81SO66FC gLoRsgTBsz0bfcvh0DsdBUPeuZb6K8zOcqiMfqAwq+ieuh6z1fExSxK5p5w1kWU+m9yUOnNi twFzvWdwxfBXS31ilulms/yicZCaC1YTQ/dgWD0QZVcYKF/Z9NBCWqqJtCrgN9kjpjhX1ZX8 U7lAV4akpzMG1Lafxn22gte0l4SqHqslH6jzjB6pDouq7KWwC3Ex+mKmAMvAmdQXyEiiF7tJ dLxlNUGRA2yaANvkhK55EH8zqwdpaJlLmCVT10aNyTxKmhjVOO3uN/gK4ZP5ZctrDkRWv61Z 1yeYrH4s10c3j+rE2ZFxT89fi2nod2jxkY80jjCai8s6iCBMchrjQ/S/tndWeJc0l9kDGFjh D/bC0L9d9il8NOIlovS5+W3VmavTJpWImHgyYKNsjf+5HU/W0Tl2arpxZu+Tk5giXyetZEiT yjDoRfib5O+0q27NbgiZUx0HBrm7ME8HIhik4w2jZVW2H4Ah5zT82BU9AW7edhdx6/6a2IAA DARxNuAqgjo3Eh+MjSD3Yv/WnG1zc5xId+3filFv0B1p9APE6qS4LFeyGF1r169sB6Xa+J0m DsZ4fQr+Dgcjv1D629Phm2NR7sVG0dfJynlkR+Fusu/oKtgb2GqabGs1UB6kIPpHPSYrwpbQ nq8ZoY6EHo68JBkKFyVmi6WiMmsaJzKYNkUrBHRjxrQk70fNscqjvRTzSM1PGXgoTsqzv59i xFylZjouY+aNyB98qWjHRdCOnv6YtNV/Dzx6MQW1s/E2oeyAtBrHSgNV5auQve4VjQfqbzuZ QOJDSF5oWyRBL7cW1aW7ks/6XnIFvXJfzmednwe0MknTwKWI1ZHxlkdWjlj2JU+E0i8zcjlO i+V/xg34Vj14ltJw+NsbVzkV3vH4R2vYXEyQYSeKxxf6kdD4V3UOIqQ9LA7GSYQ5ZCnoAGXT w7TLw1VEWEEXFCFDFH/L/Gv49fH6e2RGuu5KbPHf7yPreVUU/rAy4io18Nq+DOFN8PHOXcHb bVzwk1YQXVwANjUgR0KTDEL0S3If4idqQv9six7o8aj8ej6DQLi4Yzcbtkaed5r+h2wneKCL 7vK3Xw/c2wHkMpTgyWQm919lBYIhipjdiegC+EFvC/JFufLn7NPSgQcYGV1PddJ6KQ12k9MP 9Tag5X7zO0d7LZ9BlFbWFjmgszsa9YNJjT3NF7DAVuXcr6cLDvHx+n4ZLP6T7BMxrYx1VX4q XOAHknvMy7W3SHuTAyqOPpQgTuzORtDpMeydwYrD2X/BoGDCFXzIJp8ijs4xqcxj3XBODsHM DRyREhKq6WZ8SJShvgX841p6314Ma+Lnjbf6eTEeM5+WR5DDSFk0eRX/CZio1O6xC5BVLpzl TeA97ZT
Ironport-sdr: 66f468f7_O5Mc8Fjyklqif3bu33lP/i6HtWiCWEzdohAamsnkddCiwvM FmKfI+hBcqkYlNISHRBoFXUrguSGQoByS81FpVA==
Ui-outboundreport: notjunk:1;M01:P0:CfkZOnLweU8=;gk0cBuyzXl2OdWlhKfBqV1FeTkd 6+PkspTgVNm740QK9rzzJxCnSFL0GyrAzzpAckWgp/S3gHRmT4h7es2OGIyyw5Y8f+T4bBWaX nZITZ0AgaJMcSD+O/8nbaewkZDVvrZSIbCO7D4NKWQi30XQ0GgR+SS2X7NeG3q2bz5OsX9veI T0EdD0dZYQ8o54mL+hsWMNbN8geowULTHIAwSt6RrcfZDtHWhgKiEeU3gOjrM+3L2+j70O7dp VHGaZhtoRvZSYP1WahBHmCJIj3VdnGIaYQhZjuFudC7XAumUUXBeyTUZvSvApAHI4l4PbdX8t ZpLMsC5z7Qf4lokY4PsHnDcJ8t44YcZmw1eqctPhwpRp6hgVPpov3kgz288Yw42vwYBFlXnEz MW8ZSe4qv2rdvJzLkFvd9GiLZK8QYRVQydUk5pzSiUU/quJZqyS1Lzke7QMPltUZ0sQulu5BF +Ka6WkBoJXR7mjADDQcmhNJyYnDI3h4vRKkYixoBFsYZP5OBiWuSS//AQc4zB8SnKwbmKDod4 ChY8S4y7KZeKcIuNV5CaSJ7COwbM53xFSFKkdiSDV5DB/lydJot8jzIjo6N/szpPfrNjGkrZX ELQUrT0jx3jVTwzWD70lqmQdVyW6AZAQrw2g4r243ymkYDDtG+GlfBgH/EgwDJNM8AezZwRPW YEXzgnpuRx0ABKQw9FZ3otpHMVRHNZq6P4it+DA0KUrsxtyHjIQgmk1ungUClAu+FdEfpo7db 0FYVHtCMT3E5AcBrIdgnb9y1RKFp0yT6LAUg+IoDqMyDuUQ61S2LHxPllVMMeSA9/i2NAzy3v W0wzJmRp6yBa0KdMa07qhH8g==

Thanks for the comments. Some remarks below.

Regards
Helmut

> On 24. Sep 2024, at 12:55, peio borthelle <pborthelle AT hadoly.fr> wrote:
>
> Hi Helmut,
>
> I must admit I did not read your paper very thoroughly but on first
> impression it seems like a fun construction!

Yes, it is a fun construction. Is I said at the beginning: I wanted to design
a “Universal Turing Machine” in lambda calculus, i.e. design a lambda term
which can evaluate an arbitrary lambda term (or loop forever if the evaluated
term has no normal form).

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

Interesting similarity.

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

The universal term from your reference [3] seems to address something
different. The author wants to find a one element basis (as opposed to SKI
which is a 3-element basis). From my perspective that is a completely
different goal.

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

[Coq-Club] Simulating lambda terms in lambda calculus, Helmut Brandl, 09/24/2024
- Re: [Coq-Club] Simulating lambda terms in lambda calculus, peio borthelle, 09/24/2024
  - Re: [Coq-Club] Simulating lambda terms in lambda calculus, Helmut Brandl, 09/25/2024