https://jesper.sikanda.be/posts/1001-syntax-representations.html A better blog post on bindings forms in agda than i could write
kiselyov lambda to SKI semantically http://okmij.org/ftp/tagless-final/ski.pdf
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.
What do we do with binders?
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 bruin has some tricky points
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.
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.
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.