Advertisement
Published in:
2007 | OriginalPaper | Chapter
Games, Automata and Matching
Author : Colin Stirling
Published in: Automated Deduction – CADE-21
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Higher-order matching is the problem given
t
=
u
where
t
,
u
are terms of simply typed
λ
-calculus and
u
is closed, is there a substitution
θ
such that
t
θ
and
u
have the same normal form with respect to
βη
-equality: can
t
be pattern matched to
u
? The problem was conjectured to be decidable by Huet [4]. Loader showed that it is undecidable when
β
-equality is the same normal form by encoding
λ
-definability as matching [6].