Does anyone know the distinction between normalization and evaluation in the context of lambda calculus? I thought they were effectively the same, but then there is thing called 'normalization by evaluation':
Conversation
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
What does 'evaluation' mean in the context of the 'traditional approach'?
This Tweet was deleted by the Tweet author. Learn more
Yeah, I've been attempting to convert things to the restricted subset of expressions in my dependently typed language Pikelet. I was calling this normalization, but thought it was interchangeable with evaluation.
1
I was attempting to hackily get around having to do full substitution by just adding defs to the the context and then renormalising, but I'm now running into an issue where I'm not keeping track of captured variables.
1
Breaks down on more complicated expressions. I then tried doing an explicit substitution approach like in the PiSigma paper, but then my normal forms weren't fully reduced, so I needed to have a more interesting conversion rule.
1
I then wondered, "how do I fully reduce my 'normalised terms' into 'normal forms' as opposed to 'weak head normal forms'". Seemed like I had a gap in understanding and things were breaking down.
1
Replying to
Note that I'm also trying to avoid HOAS as is commonly used in Haskell/ML implementations, because Rust isn't as good at that stuff. (not sure, but it might lead to Rc cycles that wouldn't be cleaned up)
This Tweet was deleted by the Tweet author. Learn more
Heh, thanks for your help at any rate, slowly getting my head around things. I was trying to avoid direct substitution due to this post: siek.blogspot.com.au/2012/08/ration - but I then ran into this bug: github.com/brendanzab/pik
1
Show replies
Yup, I am, with my silly unbound clone. Tricky thing is making sure I do environments and captures correctly. 🤔
1
1
Show replies