Open colltoaction opened 3 years ago
I'm reading de Bruijn and I think we can use it to define a functor between the YAML number scalars
and Lambda calculus in de Bruijn notation
categories.
Chapter 5 in de Bruijn indices https://web.engr.oregonstate.edu/~walkiner/teaching/cs581-fa20/slides/5.LambdaCalculus.pdf
https://www.win.tue.nl/automath/archive/pdf/aut029.pdf
LAMBDA CALCULUS NOTATION WITH NAMELESS DUMMIES, A TOOL FOR AUTOMATIC FORMULA MANIPULATION, WITH APPLICATION TO THE CHURCH-ROSSER THEOREM N. G. DE BRUIJN (Comrnunicatod at tho mooting of Juno 24, 1972) In ordinary lambda calculus the occurrences of a bound variable are made recognizable by the use of one and the same (otherwise irrelevan+) name at all occurrences. This convention is known to cause considerable trouble in cases of substitution. In the present paper a different notational system is developed, where occurrences of variables are indicated by integers giving the "distance" to the binding L instead of a name attached to that A. The system is claimed to be efficient for automatic formula manipulation as well as for metalingual discrission. As an example the most essential part of a proof of the Church-Rosser theorem is presented in this namefree calculus.
We can think of the de Bruijn notation as a lower level lambda calculus form. Closer to the machine.
This is explained in the previous paper. It could be useful to write the first bootstrapping tools as in #5.
Maybe a list is de Bruijn notation and a mapping classical notation
Different approaches for mixing named and nameless variables appear in the literature:
In this paper, we name free variables (ie, variables bound in the context) so that we can refer to them and rearrange them without the need to count; we give bound variables de Bruijn indices to ensure a canonical means of reference where there’s no ‘social agreement’ on a name
At its core,
yaml.yaml
just wants to be a functor that maps between the yaml and lambda categories.With yaml we get a human friendly data serialization standard for all programming languages. More specifically I see:
On the other hand, the yaml spec is pretty dense and we don't want to deal with everything from the beginning.
The mapping to lambda is not just for the math, but we actually want to run software in a computer. In #2 I took a lambda calculus interpreter written in Rust and I was able to map simple documents to lambda terms.
A different approach could map between languages (transpiling). Haskell seems to be the closest but I'm not familiar with the syntax or tooling.