Hello. On 07/04/18 01:45, Thomas Tuerk wrote: > higher order matching is decidable, but has a very high complexity. (see > e.g. "An introduction to decidability of higher-order matching", Colin > Stirling, http://homepages.inf.ed.ac.uk/cps/newnewj.pdf). Higher order > unification is undecidable, but matching is decidable I see, thanks for the clarification and the useful link.
> As I understand it, HOL supports higher-order patterns for higher-order > matching. This > has polynomial complexity. In case you use anything else than a > higher-order pattern (slightly extended), all bets are off. It might > work or fail. > I can't remember, where I got this belief that HOL supports higher-order > patterns. Looking for some reference, I could not find much > documentation either, but Section 7.5.4.4 in the description manual > seems to hint in this direction I noticed that PAT_ASSUM and X_PAT_ASSUM rely on hypotheses like “∀x. x ≤ 1 ⇒ ...” matching (according to “ho_match_term”) “∀x. x ≤ 1 ⇒ P”, even though the substitution for “P” would need the free instances of “x” to be captured by the abstraction. Do you know what other parts of HOL rely on using “ho_match_term” for higher-order matching on something else than patterns?. Regards.
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
