[Agda] Defining large numbers without recursion, with short programs

[Martin Escardo]

On 11/03/15 01:29, Aaron Stump wrote:
> It is very interesting to see this example in Agda, and I enjoyed
> reading your explanation.
>
> You mentioned you are not sure if iteration of N is a new technique.  I
> believe you can find this (presented quite a bit more densely!) in some
> papers by Daniel Leivant, exploring the computational power of
> predicative polymorphism.  See his CMU tech report "Finitely stratified
> polymorphism" (there is also a LICS '89 paper on the topic):
>
> http://repository.cmu.edu/compsci/1962/

Thanks! The definition of N is indeed at the top of page 6. In my
message, I am a bit more spartan than the above paper, in that I only
consider the simply typed lambda calculus. But yes, the technique is
there.

I've updated the above agda file and its html rendering with a link to
your message, and also with a quote of your paragraph with the
reference.

Best wishes,
Martin

>
> Cheers,
> Aaron
>
> On 03/10/2015 07:49 PM, effectfully wrote:
>> Neat trick. BTW, you can avoid these giant implicit arguments by
>> wrapping the N into a record (my emacs doesn't want to display 𝟘 𝟙
>> 𝟚 𝟛 properly):
>>
>> {-# OPTIONS --no-pattern-matching #-}
>>
>> U = Set
>>
>> data ℕ : U where
>>   zero : ℕ
>>   succ : ℕ → ℕ
>>
>> record N X : U where
>>    constructor #
>>    field el : (X → X) → (X → X)
>> open N
>>
>> b0 b1 b2 b3 : {X : U} → N X
>> b0 = # λ s z → z
>> b1 = # λ s z → s z
>> b2 = # λ s z → s(s z)
>> b3 = # λ s z → s(s(s z))
>>
>> suc : {X : U} → N X → N X
>> suc n = # λ s z → s (el n s z)
>>
>> add : {X : U} → N X → N X → N X
>> add m n = # λ s z → el m s (el n s z)
>>
>> N-rec : {X : U} → (X → X) → X → (N X → X)
>> N-rec s z m = el m s z
>>
>>
>> mul : {X : U} → N X → N(N X) → N X
>> mul m = N-rec (add m) b0
>>
>> exp : {X : U} → N(N X) → N(N X) → N X
>> exp n = N-rec (λ m → mul m n) b1
>>
>> decode : N ℕ → ℕ
>> decode = N-rec succ zero
>>
>> large : ℕ
>> large = decode
>>   (exp b2
>>   (exp b2
>>   (exp b2
>>   (exp b2
>>   (exp b2
>>   (exp b2
>>   (exp b2
>>   (exp b2
>>   (exp {?} b2
>>        b2)))))))))
>>
>> Then Agda infers
>>
>>      N (N (N (N (N (N (N (N ℕ)))))))
>>
>> in the hole above.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe