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!

$\endgroup$
  • 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 Sep 22 '16 at 7:11
  • $\begingroup$ @AndrejBauer Maybe it is a abbreviation as you said. let me check more sources $\endgroup$ – alim Sep 23 '16 at 6:26
  • 2
    $\begingroup$ No, do not check more sources! Tell us instead what sources you are using. $\endgroup$ – Andrej Bauer Sep 23 '16 at 7:27
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;
$\endgroup$
  • $\begingroup$ I saw Benjamin's book mentioned an abbreviation " \/X.T =def= \/X<:Top.T ". I guess that is why. Thanks. $\endgroup$ – alim Sep 30 '16 at 11:32

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.