Binding Forms
https://jesper.sikanda.be/posts/1001-syntax-representations.html A better blog post on bindings forms in agda than i could write
2021-03
kiselyov lambda to SKI semantically http://okmij.org/ftp/tagless-final/ski.pdf
http://math.andrej.com/2012/11/29/how-to-implement-dependent-type-theory-iii/#:~:text=de%20Bruijn%20levels%20are%20positions,the%20top%20of%20the%20stack.
https://cs.stackexchange.com/questions/119861/semantics-for-de-bruijn-levels
Yes so, Semantic of de bruijn z really is a projection function from a tuple s is a reduction function ignoring They really use polymorphism to achieve what they need here. i + l = n levels plus indices = number of binders. I can be wokring in Fock space for homogenous operators. Simon here shows a homogenous list based semantics.
2020-07
What do we do with binders?
https://www.schoolofhaskell.com/user/edwardk/bound
Do Just dumbass names
https://www.cs.cornell.edu/courses/cs3110/2019sp/textbook/interp/subst_lambda.html ordinary stringy substituion done right possibly
<code>data Lambo = Var String | Lam String Lambo | App lambo Lambo
-- nope i fucked this up. lordy
-- You need to alpha rename if x contains s' as a free var
subst (Lam s' b) s x | s == s' = (Lam s' b)
| otherwise = Lam s' (subst b s x)
subst (Var s') s x | s == s' = x
| otherwise = Var s'
subst (App f x) s x = App (subst f s x) (subst f s x)
but then we want to be lazy about substituions.
eval :: Lambo -> Lambo
eval (App f x) = let x' = eval x in
eval (App (Lam s b) x) = eval (subst b s x)
eval (App f x) | reducible f = let f' = eval f in eval f' x -- if we also let x' = eval x it is cbv
| otherwise = (App f x)
eval x = x</code>
barendregt convention - bound variables are uniquely named. The rapier.
de Bruijn.
de bruin has some tricky points
<code></code>
Direct Substitution
Environment passing
Well typed de bruijn. http://docs.idris-lang.org/en/latest/tutorial/interp.html
Bird and Patterson, Altenkirch and Reus. Look at Eisenberg’s Stitch. and Idris tutorial.
https://plfa.github.io/DeBruijn/
http://www.cs.ox.ac.uk/people/richard.bird/online/BirdPaterson99DeBruijn.pdf
Chris mentioned https://nms.kcl.ac.uk/christian.urban/Publications/nom-tech.pdf nominal forms in isabelle. I don’t know what this is
HOAS. Weak HOAS, PHOAS.
Locally nameless. Separate free and bound variables. Conor Mcbride and Charuand paper
Point-free style. Does my point-free guide hold some stuff about binding forms?
Map -style. This one is new to me. Conor Mcbride’s Everybody’s got the be somewhere mentions this. At every lambda, you hold a map of where those variables end up going. This leads to a lot of duplication of structure, but it makes sense. Even de Bruijn indices are a peculiar indirection. https://arxiv.org/pdf/1807.04085.pdf
I had some notes I was doing for indexful differentiation. Tensor expressions. It was an interesting exercise
Differentiation is syntactic, not semantic. That’s why is sucks so hard in thermo
Differential is a binding form itself. See a comment in Functional Differential geometry and in Plotkin’s talk.
weirich https://www.youtube.com/watch?v=j2xYSxMkXeQ
https://github.com/sweirich/challenge/blob/canon/debruijn/debruijn1.md
In locally nameless we don’t have to shift on the term we’re substituting in since the free variables in the term have names.