Conversation

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

en.wikipedia.org

Normalisation by evaluation - Wikipedia

aaron

@aatxe

Apr 23, 2018

Normalization is more broad, I think. I.e. it’s any method of getting terms into normal form. The linked one uses a denotational semantics. You can also use an operational semantics. And probably someone, somewhere, has even crazier ways of doing normalization that I don’t know.

aaron

@aatxe

Apr 23, 2018

Oh, sorry, Tweetbot didn't show me the rest of the thread for whatever reason.

Brendan Zabarauskas

@brendanzab

Apr 23, 2018

Thanks for the reply anyway! So could you say that 'evaluation' is a form of normalization?

aaron

@aatxe

Apr 23, 2018

Yeah, something like that! In practice, I'm probably also guilty of using them interchangeably though. 😊

Brendan Zabarauskas

@brendanzab

Replying to

@aatxe

I also wrote out this thing on different normal forms to try and get my head around it - not sure how correct it is though: gitter.im/pikelet-lang/L - gist is, 'strict evaluation is normalization via HNF', and 'lazy evaluation is normalization via WNF'

2:34 PM · Apr 23, 2018Twitter Web Client