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

[Conor McBride]

Yong Luo wrote:
> I wrote:
>
>   
>> 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?
>   

Are you saying that the constant factor is important? Maybe it is, and 
maybe not. One might also question whether comparing numbers of 
reduction steps makes any sense when UTT reductions are very simple and 
pattern matching requires a more complex combination of constructor 
comparison and tuple unpacking operations. As it happens, the UTT code 
is quite similar to the Augustsson-style efficient compilation of 
pattern matching.

If the constant factor is important to you, I'm sure you can calculate 
it yourself.

All the best

Conor


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.