Re: Working with lambda abstraction capturing binding effects

Dear Dale,

thanks for your reply.

Am 23.11.12 09:22, schrieb Dale Miller:
> Dear Jakob,
>
> I'll respond to your questions via the mailing list as well.
>
>     infixr ==> 3.
>
>     % quantifiers
>     type all term -> form -> form.
>     type some term -> form -> form.
>
>
> I believe that the types for the quantifiers here should be 
> (term -> form) -> form.
>  
Sure thank you. The arrow associates to the right. This happened during
the second transscript - My module/signature is of the propper type ;-)
>
>
>     Is there an elegant solution to this?
>
>
> Sure.  You can write a couple of simple predicates such as these:
>
> head A Body :- frm F, instan F (Body => A).
> instan (all B) C :- instan (B T) C.
> instan (B ==> A) (B ==> A).
>
> Here, 
> ?- head (q a) B.
> should instantiate the B to all those instances of clauses that imply
> (q a).  The material in section 7.2 (page 180) of Programming in
> higher-order logic <https://sites.google.com/site/proghol/> is
> probably the most closely related to your email.
>

Frankly I reread  that chapter yesterday evening - almost wanting to
answer myself. The very nice thing is that by having to apply the
abstraction B with an unbound variable T in order to unify with C gives
access to the variable, so I can for instance collect them. Since the
lambda variable is substituted by T (beta contraction) T is also used
inside Body. Nice.

type head   form -> form -> list term -> o.
type instan form -> form -> list term -> o.

head A Body Vars :- frm F, instan F (Body ==> A) Vars.
instan (all B) C (T :: Vars') :- instan (B T) C Vars'.
instan (B ==> A) (B ==> A) nil.

Thanks again.

Best,
Jakob

_______________________________________________
Lprolog mailing list
[email protected]
https://wwws.cs.umn.edu/mm-cs/listinfo/lprolog