4
$\begingroup$

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))) 
$\endgroup$
0

1 Answer 1

3
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$
    – joseville
    Nov 14, 2021 at 4:33

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .