Encoding of the generalization function for PL

[Jinxu Zhao]

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]

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.

  -Dale

--
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.