1

I am not sure how to interpret this term. My first thought is that it is this an application of $x$ to $\lambda y.\lambda z.x$ Is that the correct interpretation or is it not reducible?

mcmapple
  • 121
  • 1
    Could you provide a bit more context on your notation? – DominikS Nov 28 '23 at 14:26
  • Yes, you are correct. @DominikS This is lambda calculus which is standard notation in the theory of computation and the foundation of functional programming languages like Haskell or Scala. – John Douma Nov 28 '23 at 14:56

1 Answers1

4

Indeed, the only possible parsing of this expression is “$x$ applied to $λy.λz.x$”. In general, standard conventions for writing λ-terms are the usual “Barendregt” one, or the Krivine notation. One should make clear the notation they use when writing λ-terms.

By the way, be careful with the words you are using:

  • to interpret a λ-term is something else, it usually refers to giving it a semantics in a model;
  • this term is not reducible, at least for the standard notion of reduction (aka. β-reduction), since it does not contain any β-redex.
sparusaurata
  • 438