Re: [isabelle] Higher-order matching and unification

Am 26/06/2012 05:55, schrieb Steve Wong:
> 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?

The flex-rigid terminology only refers to the head symbol, whereas in matching
the whole term must be closed. Colin Stirlin proved that HO matching is decidable.


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