[Agda] Some problems with K-S basis

[G. Allais]

> How to bring there typed combinators, typed lambdas, I do not know.
> May be, people can explain.

Dybjer and Coquand have a really nice paper about normalisation
by evaluation for pure typed combinatory logic:

http://www.cse.chalmers.se/~peterd/papers/GlueingTypes93.pdf

On 24/07/17 13:22, Sergei Meshveliani wrote:
> On Mon, 2017-07-24 at 18:32 +1000, v0id_NULL wrote:
>> Dear list,
>> Help me, please. I try to deal with combinatory logic via Agda, but I
>> have some problems with defining of K-combinator. If I define K and S
>> combinators like this
>>
>>
>> K : {a b : _} → {A : Set a} → {B : Set b} → A → B → A
>> K x _ = x
>>
>>
>> S : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → (A → B →
>> C) → (A → B) → A → C
>> S x y z = x z (y z)
>>
>>
>> this leads to that Agda can not solve some constrains in this
>> definition of I-combinator
>>
>>
>> I : {ℓ : _} → {A : Set ℓ} → A → A
>> I = S K K
>>
> 
> I am not sure, 
> but I suspect that if we represent the combinators as Agda functions of
> types like (A → B → A), (A → B → C) → (A → B) → A → C),
> and such, this will mean that Agda is required to assign correct types
> to the algorithms representing combinators. 
> But is this at all possible? 
> Can Agda correctly assign a type to the Y combinator, if combinators are
> expressed as the above functions?
> 
> Can anybody, please, make it clear?
> 
> I see the following safe construct:
> 
> -----------------------------------------------------
> open import Function using (case_of_)
> open import Relation.Binary using (Rel)
> open import Data.Maybe using (Maybe; just; nothing)
> 
> data KS-term :  Set
>      where
>      K   : KS-term
>      S   : KS-term
>      app : KS-term → KS-term → KS-term  	-- application
> 
> I :  KS-term               -- I combinator
> I =  app (app S K) K
> 
> step : KS-term → Maybe KS-term    -- one step of evaluation 
> 
> step (app (app K x) _)         =  just x
> step (app (app (app S x) y) z) =  just (app (app x z) (app y z))
> step t                         =  nothing
>                                        -- t  is in normal form
> --------------------------------------------------------------------
> 
> (I do not recall now, are the K-S things correctly written?).
> 
> 
> {- this must not terminate, for some arguments:
>   
> evaluate : KS-term → KS-term
> evaluate t =  case step t of \ { nothing  → t                          
>                                ; (just u) → evaluate u } 
> -}
> 
> 
>> Generaly, tell me, please, is it good idea to implement something like
>> combinatory logic via Agda?
>>
> 
> Also it is possible to express in Agda the equivalence relation _=ks_
> for  (s t : KS-term).  
> t =ks u  when there are given the sequences steps1 and steps2 of steps
> like `step' above, such that applying  steps1 to t  yields the same term
> as applying steps2 to  u.  And may be, a step needs to be applied to a
> subterm, not necessarily at top.
> 
> In this model, one could develop some prover that would solve
> equivalence of functional programs (in untyped model, though) for easy
> examples, and would fail in complex cases.
> 
> How to bring there typed combinators, typed lambdas, I do not know. 
> May be, people can explain. 
> 
> Also, may be, there also exist some Agda libraries for combinatory
> logic? 
> 
> How to bring there typed combinators, typed lambdas, I do not know. 
> May be, people can explain. 
> 
> Anyway, the main thing here is to formulate clearly for oneself:  
> what is the goal of the project.
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170724/e0c4eee9/attachment.sig>