Re: Working with lambda abstraction capturing binding effects

Dear Jakob,

I'll respond to your questions via the mailing list as well.

I am trying to get this sorted out.
> I would like to encode an object level logic following the conventions
> of Programming with Higher-Order Logic.
>
> % categories
> kind term type.
> kind form type.
>
> % connectives
> type ==> form -> form -> form.
> type &&    form -> form -> form.
>
> infixl && 5.
> 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.


> % predicate symbols
> p: term -> form.
> q : term -> form.
>
> % term constant symbols
> a: term.
> f: term -> term.
>
> To introduce some object formulae as knowledge I use a predicate frm
>     type frm form -> o.
>
> such that I know for instance:
>     frm (p a ==> q a).
>     frm (all x\ all y\ p x && r y ==> q y).
>
> Now I would like to uniformally treat qantified and ground formulae in
> reasoning about them; Just assume for the sake of the example I would
> like to unify all formuale that imply q a.
> Naively I would try something like
>     frm F (X ==> q a).
>
> 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.

Hope this helps.  -Dale

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