0
$\begingroup$

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?

source1

Thanks in advance!

Improve this question
$\endgroup$
3
  • 6
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Sep 22, 2016 at 7:11
  • $\begingroup$ @AndrejBauer Maybe it is a abbreviation as you said. let me check more sources $\endgroup$
    – alim
    Commented Sep 23, 2016 at 6:26
  • 2
    $\begingroup$ No, do not check more sources! Tell us instead what sources you are using. $\endgroup$
    – Andrej Bauer
    Commented Sep 23, 2016 at 7:27

1 Answer 1

Reset to default
2
$\begingroup$

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;
Improve this answer
$\endgroup$
1
  • $\begingroup$ I saw Benjamin's book mentioned an abbreviation " \/X.T =def= \/X<:Top.T ". I guess that is why. Thanks. $\endgroup$
    – alim
    Commented Sep 30, 2016 at 11:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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