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.

Tobias





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