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?
Thanks in advance!