In Girard, Proofs and Types, the operator successor is defined as follows: $St\equiv\Lambda X.\lambda x:X \lambda y:X\to X.y(tXxy)$, while $0\equiv\Lambda X.\lambda x:X \lambda y:X\to X.x$. If I try to compute $S0$, I get (using $\alpha$-reduction even if it might not be necessary):

$\S0\equiv\Lambda X.\lambda x:X \lambda y:X\to X(\Lambda U.\lambda u:U\lambda v:U\to U.uXxy)$

$\to_\beta\Lambda X.\lambda x:X\lambda y:X\to X.y(\lambda u:X\lambda v:X\to X.u(xy))$

$\to_\beta\Lambda X.\lambda x:X\lambda y:X\to X.y(\lambda v:X\to X.xy)$ and now I cannot substitute since $y$ is free in the latter term; even in I apply a new $\alpha$-conversion the result won't look as a numeral at all.

If I try the same procedure, without use of the conversion, I get as a result

$\Lambda X.\lambda x:X\lambda y:X\to X.xy$, which is nicer but still wrong. Now, where am I making mistakes and which one of the approch should I use? I think I sould start with $\alpha$-conversion, as, in principle, the variables $x,y$ are referred to $S$ and not to $0$., but this computation leads me to a very confusing output.

Since I was asked in the comment to clarify notations and unfortunately I did not found many discussions regarding system F:

$\Lambda$ is the symbol of universal abstraction, $\lambda$ is the symbol for terms abstraction, capital letters rapresent types, while small ones are term variables. Writing $x:X$ I mean the term $x$ inhabitates the type $X$.

  • $\begingroup$ Could you give a link to a discussion of the notation/operators etc being used? E.g. what are the upper/lower case lambdas, and $U.$ $\endgroup$ – coffeemath Jan 23 '17 at 16:05
  • 1
    $\begingroup$ @coffeemath I edited the post, I hope this helps you a bit. $\endgroup$ – user275116 Jan 23 '17 at 16:42

Your calculations are wrong. In fact, they just don't make any sense. Your initial expansion of $S0$ doesn't match the definition, and then you seem to be "reducing" things when your terms have no $\beta$ redexes. $\alpha$-conversion correctly applied never changes the normal form, so it would never lead you to get different answers. Note $tXxy$ means $((tX)x)y$. $\beta$-reduction is $(\lambda x:X.E)y \to E[x\mapsto y]$ where $E[x\mapsto y]$ means $E$ with all occurrences of $x$ replaced with $y$ in a capture-avoiding way. Similarly for $\Lambda$. Also, while they are often omitted, compound terms are implicitly wrapped in parentheses. So $0 \equiv (\Lambda X.\lambda x:X.\lambda y:X\to X.x)$ or to be completely explicit $(\Lambda X.(\lambda x:X.(\lambda y:(X\to X).u)))$. Your expansion of $S0$ may be a mixture of a typo and failing to include parentheses.

The Church-numeral for the natural number $n$ is the $\lambda$-term of the form $$\Lambda N.\lambda z:N.\lambda s:N\to N.s^n z$$ where $s^n z$ is shorthand for for $s$ applied to $z$ $n$-times, e.g. $s^3z = s(s(sz))$. $s^0 z = z$ and so you can verify that the $\lambda$-term for $0$ is indeed the Church-numeral for the number $0$.

The calculation proceeds as follows, note that in this case at every point there is only one possible $\beta$-redex: $$\begin{align} S0 & \equiv \Lambda X.\lambda x : X.\lambda y:X\to X.y(0Xxy) & \text{by definition of }S \\ & \equiv \Lambda X.\lambda x : X.\lambda y:X\to X.y((\Lambda U.\lambda u:U.\lambda v:U\to U.u)Xxy) & \text{by definition of 0 and }\alpha \\ & \to \Lambda X.\lambda x : X.\lambda y:X\to X.y((\lambda u:X.\lambda v:X\to X.u)xy) & \beta\text{ reduction} \\ & \to \Lambda X.\lambda x : X.\lambda y:X\to X.y((\lambda v:X\to X.x)y) & \beta\text{ reduction} \\ & \to \Lambda X.\lambda x : X.\lambda y:X\to X.yx & \beta\text{ reduction} \\ \end{align}$$

This is its normal form. Further, it is $\alpha$-equivalent to the Church-numeral for $1$.

  • $\begingroup$ Thanks a lot, I get very confused with association rule $\endgroup$ – user275116 Jan 23 '17 at 20:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.