3
$\begingroup$

(NB: λ-calculus n00b here!)

I derive the following: $$ \lambda x.\lambda y.xy \equiv \lambda x.(\lambda y.xy) \equiv \lambda x.x $$

To check myself, I tried to reduce the same expression with several online "λ-calculus calculators" (e.g. the λ Calculus Calculator or Lambda Calculator), and, to my surprise, they all agree that the original expression ($\lambda x.\lambda y.xy$) is already in normal form (and therefore, no further reductions are possible).

Where does my derivation go wrong?

My derivation consists of two "moves": (1) "insertion of parentheses" (just to make the evaluation order explicit), and (2) one reduction, namely $\lambda y.xy \equiv x$. The latter is an instance of what the book I am following1 calls an "η-reduction." I figure that one of these two moves must be wrong, but I can't see how.

(FWIW, I do agree with these online calculators that the similar-looking expression $\lambda x.\lambda y.yx$ is in normal form.)

1 Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory (1977) by Joseph E. Stoy.

$\endgroup$
0

2 Answers 2

Reset to default
7
$\begingroup$

'Normal form' typically means '$\beta$ normal form' and not '$\beta\eta$ normal form', so your $\eta$-reduction step is not allowed by the normal form calculators.

$\endgroup$
1
$\begingroup$

As a complement to the accepted answer, in typed lambda-calculus $\lambda x.x$ has the type $a \rightarrow a$, whereas $\lambda x.\lambda y. x~y$ has the type $(a \rightarrow b) \rightarrow a \rightarrow b$.

In a statically typed functional programming language such as Miranda, Haskell, Clean, F# or Elm, the former would be the identity function, whereas the latter would be the apply forward (or pipe into) operation (a fact made evident by $\alpha$-renaming the arguments: $\lambda f.\lambda x. f~x$).

In the Curry-Howard correspondence, the former function corresponds, according to its type, to the trivial identity tautology (if a then a), whereas the latter corresponds to modus ponens.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.