Exponentiation in Lambda Calculus

I just need a double check.

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)))


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...

• thanks! Gotcha, good point. I thought it was self-inconsistent because they used EXP = one thing, then EXP = another thing and the one thing was not exactly equal to the another thing. Nov 14, 2021 at 4:33