[isabelle] Higher-order matching and unification



Hi,

I see that higher-order pattern matching is a decidable fragment of
higher-order unification. With matching, one of the expressions must be
closed. So does that mean HO pattern matching is essentially a flex-rigid
problem? If so, does that mean unifying a flex-rigid pair is guaranteed to
be decidable?

Thank you for your time.

Steve




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.