# having issue with numbers in Polymorphic Lambda Calculus

It is said that Church Numbers are encoded as following

   c0 = λX. λs:X->X. λz:X. z;
c1 = λX. λs:X->X. λz:X. s z;
c2 = λX. λs:X->X. λz:X. s (s z);
c3 = λX. λs:X->X. λz:X. s (s (s z));


The church numbers are terms, right? but the terms are given by the following syntax.

  t ::=                          terms
x                          //variable
λx:T.t                     //abstraction
t t                        //application
λX<:T.t                    //type abstraction
t [T]                      //type application


It seems church numbers do not respect the syntax of terms to me, strange.

I think it should be like

      c0 = λX<:some type here. λs:X->X. λz:X. z


So, how to write church numbers in a consistent way?

If possible provide simple examples to explain, i.e. 2 * 2, how to write this?

• You are misreading syntax. It is likely that you are reading a text which uses some abbreviations. It would help if you gave us a reference where you got the material from. There is no single established way to write the terms of the $\lambda$-calculus. If you are getting this from two different sources, then you should expect that some adjustment to syntax is needed. – Andrej Bauer Sep 22 '16 at 7:11
• @AndrejBauer Maybe it is a abbreviation as you said. let me check more sources – alim Sep 23 '16 at 6:26
• No, do not check more sources! Tell us instead what sources you are using. – Andrej Bauer Sep 23 '16 at 7:27

The syntax you written is probably of the System F<:.

However, the typed Church numerals you written are introduced in the context of System F (a.k.a. λ2) at Fig. 11 of the source pdf.

The terms of System F are defined like below in Types and programming languages (Benjamin C. Pierce, MIT press, 2002):

t ::=           terms:
x         variable
λx:T.t    abstraction
t t       application
λX.t      type abstraction
t [T]     type application


The typed Church numerals at Fig. 11 are terms in this definition.

Moreover, in System F<:, Church numerals are also well-typed and can be more generalized. Below examples are taken from Types and programming languages. Top is the maximum type.

szero = λX<:Top. λS<:X. λZ<:X. λs:X→S. λz:Z. z;
sone  = λX<:Top. λS<:X. λZ<:X. λs:X→S. λz:Z. s z;

• I saw Benjamin's book mentioned an abbreviation " \/X.T =def= \/X<:Top.T ". I guess that is why. Thanks. – alim Sep 30 '16 at 11:32