[Agda] Some problems with K-S basis

[Sergei Meshveliani]

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