[TYPES] An efficient program for the function (mod 3) in type theories

[Yong Luo]

Hi Conor,

Thank you.

Sent: Thursday, November 23, 2006 8:42 AM
Subject: Re: [TYPES] An efficient program for the function (mod 3) in type
theories


> Hi Yong
>
> Yong Luo wrote:
> > [ The Types Forum,
http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> >
> > Dear all,
> >
> > I am looking for an efficient program of the following function in the
> > Martin-Lof's type theory or UTT.
> >
>
> As well you know, I wrote a program which will spit out the program you
> want, given (more or less) the program you've written.
>
> > f :: Nat -> Nat
> >
> > f (zero) = zero
> > f (succ(zero)) = succ(zero)
> > f (succ(succ(zero))) =  succ(succ(zero))
> > f (succ(succ(succ(x)))) = f (x)
> >
>
> > In the Martin-Lof's type theory or UTT, every function is defined by
> > eliminators of inductive data types. I would like to know whether it is
> > possible to have an efficient program for the function f.
> >
>
> Yes it is. The pattern matching equations hold computationally for the
> UTT programs which the translation spits out. Given a suitable reduction
> strategy (ie, one designed to exploit this property of the translation),
> you get a constant factor blowup in the number of steps, ie a larger
> number of smaller steps.
>
> Hope this helps

There is no doult that the function "mod 3" can be defined in the UTT, for
example, by using pairs or similar things. My question is: what is the most
efficient program in the UTT for this function?  I would also like to know
how many reduction steps for f(100), roughly?

Thank you,

Yong