Exponentiation in Lambda Calculus

I just need a double check.

Some recitation notes say:

EXP $= λmn.m$ $($MUL $n)$ $\underline{1}$.
The notes also say: EXP $= λmn.nm$

I think I found an inconsistency and would like someone to double check if that's appropriate for this site:

Let $\underline{m}$ and $\underline{n}$ be Church numerals representing natural numbers $n$ and $m$ respectively. More specifically, $\underline{m} = λfx.f^mx$, where $f^m$ is the $m$-fold composition of $f$ and likewise for $\underline{n}$. When applied to EXP as EXP $\underline{m}$ $\underline{n}$ I get inconsistent results:

• With EXP $= λmn.m$ $($MUL $n)$ $\underline{1}$
  • EXP $\underline{m}$ $\underline{n} = \underline{n^m}$.
• In contrast, with EXP $= λmn.nm$
  • EXP $\underline{m}$ $\underline{n} = \underline{m^n}$

Using an Online Lambad Calculus interpreter, I confirmed that with EXP $= λmn.nm$, EXP $\underline{2}$ $\underline{3} = \underline{2^3} = \underline{8}$

This is the input into the online interpreter that corresponds to $(λmn.nm)$ $\underline{2}$ $\underline{3}$:

(lambda m n.n m) (lambda f x. f(f x)) (lambda f x.f(f(f x))) 

Solution 1:

I agree with you it's confuing here as referenced here:

$exp~ m~ n = m^n = nm$

which gives the lambda expression, $exp \equiv \lambda m.\lambda n.nm$

So its second definition means $m^n$ after applying to $m$ and $n$ consecutively. While as explained above your first definition of EXP:

exponentiation is iterated multiplication:

So you need to read the first definition as $m$ should be at the exponent position and $n$ should be at the base position after applying to $m$ and $n$ consecutively. So there's no inconsistency here, just need to be careful about how to read and interpret these 2 similar but subtly different definitions...