0
$\begingroup$

The way I see it, it should not be further reducible. I'm thinking λz.zq is like

lambda z: z(q) # Python, not lambda calc

and you do not know z nor q so it is not further reducible.

The below derivation (where I am wondering about the last steps) is from the new Haskell book:

enter image description here

$\endgroup$
1

1 Answer 1

3
$\begingroup$

It is $\beta$-reduction defined in terms of substitution (rename ($\alpha$-conversion) first if necessary):

$$(\lambda z. zq) (q) \to_{\beta} [z/q](zq) = qq. $$


In Haskell, $\lambda z.zq$ defines an anonymous function which takes a single parameter (represented by $z$) and performes $zq$.

$\endgroup$
1
  • $\begingroup$ Now that I understand the mechanics of lambda calc better I see that this was just a straightforward application of the rules. Thanks though. $\endgroup$ Commented Jan 30, 2016 at 11:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.