[TYPES] Eliminators in type theory
Jonathan Seldin
jonathan.seldin at uleth.ca
Fri Mar 17 14:15:41 EST 2006
If you are talking about a functional language that includes pure
lambda-calculus, you might be interested in the discussion in Curry,
Hindley, and Seldin, Combinatory Logic, vol. II (North-Holland,
1968), section 13D. Here R is Elim_Nat. Definitions of Elim_Nat and
pairs are given in terms of an iterator (called Z), which takes each
numeral to its corresponding Church numeral (\xy.x(x(...(xy)...)),
where there are n x's after the dot), and since this iterator can
easily be defined in terms of Elim_Nat, the definitions would work in
the proposed system. This shows, I think, that fib could be defined
in the proposed system without the numerical coding of pairs.
But this contains no information about efficiency.
On 17-Mar-06, at 8:32 AM, Ulrich Berger wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/
> types-list ]
>
> Even if you disallow function types as result type of an elimination,
> coding of two numbers into a single one as well as the corresponding
> projections can be defined (old stuff in books on computability theory
> or logic).
>
> Uli
>
> Andreas Abel wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/
>> types-list ]
>>
>> Pairs can be simulated by with higher-order primitive recursion. For
>> instance, the following (Haskell) functions 'iter' and 'fib' are
>> definable in type theory with function spaces, natural numbers, and
>> eliminators alone.
>>
>> iter :: Int -> Int -> Int -> Int
>> iter k l 0 = k
>> iter k l (n+1) = iter l (k+l) n
>>
>> fib :: Int -> Int
>> fib = iter 0 1
>>
>> fibs = [ fib i | i <- [0..]]
>>
>> test = take 15 fibs
>> -- [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377]
>>
>> Maybe you have to reformulate your question, such that the
>> eliminators
>> can only produce something of base type, e.g., inductive type, but
>> not
>> function type. Then, the Ackermann function is not definable.
>>
>> Cheers,
>> Andreas
>>
>> Yong Luo wrote:
>>
>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/
>>> types-list ]
>>>
>>>
>>> I would like to understand how powerful the eliminators of
>>> inductive types
>>> can be in type theory.
>>>
>>> Suppose a type system has the type of natural numbers ONLY, that
>>> is, we have
>>> only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and
>>> its two
>>> computation rules.
>>>
>>> Can we define fib function in such a system? Note that we don't
>>> have pairs
>>> and function types.
>>>
>>> fib 0 = 1
>>> fib 1 = 1
>>> fib (n+2) = fib n + fib (n+1)
>>>
>>> In such a system, we know some functions can be defined, for
>>> example,
>>> plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
>>> If we add the type of pairs, then more efficient fib can be
>>> easily defined.
>>>
>>> Thanks,
>>>
>>> Yong
>>> ==============================
>>> Dr. Yong Luo
>>> Computing Laboratory
>>> University of Kent
>>>
>>>
>>
>>
>>
Jonathan P. Seldin tel: 403-329-2364
Department of Mathematics and Computer Science jonathan.seldin at uleth.ca
University of Lethbridge seldin at cs.uleth.ca
4401 University Drive http://www.cs.uleth.ca/~seldin/
Lethbridge, Alberta, Canada, T1K 3M4
More information about the Types-list
mailing list