Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Higher-order matching and unification

Email Gateway (Aug 18 2022 at 20:14):

From: Steve Wong <s.wong.731@gmail.com>
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

Email Gateway (Aug 18 2022 at 20:14):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Last updated: Nov 21 2024 at 12:39 UTC