Encoding of the generalization function for PL

Skip to first unread message

Jinxu Zhao

Mar 20, 2018, 1:40:50 PM3/20/18
to Abella
Hi all,

I would like to know if it is possible/easy to encode the generalization function/relation in Abella.

For Hindley-Milner, the generalization relation states like: if G |- e : t, a \not\in free(G), then G |- e : \forall a. t

Correct me if I am wrong, we need to
1. collect the set(list) of free variables in t, which is basically a traversal through the structure of types, where duplicated variable names should be taken good care
2. "generalize" t through Abella's HOAS, say, gen (var a :: fvs) (t a) r := gen fvs (all t) r

But the approach I thought seems complicated (or quite algorithmic), and I would like to know if any other encodings may look better.

Or is it common to encode the generalization relation abstractly? (Something like the HM declarative generalization relation stated above) And how?

Thanks anyway for your attention and help!

Dale Miller

Mar 24, 2018, 5:42:11 AM3/24/18
to abella-the...@googlegroups.com
I don't know any way to implement the generalization step you describe without writing your own unification algorithm and encoding your own "logic variables".  If you rely on the unification in Abella or in lambda Prolog, then you really can't make the generalization step you want.   There is no way, in that setting, to get an encoding of the most general unifier (the only one you want for this generalization step).  

Fortunately, encoding your own unification algorithm should not be too difficult in Abella or lambda Prolog.


You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-prover+unsub...@googlegroups.com.
To post to this group, send email to abella-theorem-prover@googlegroups.com.
Visit this group at https://groups.google.com/group/abella-theorem-prover.
For more options, visit https://groups.google.com/d/optout.

Reply all
Reply to author
0 new messages