coq-library-undecidability icon indicating copy to clipboard operation
coq-library-undecidability copied to clipboard

Published 20 hours ago • verified publisher icon uds-psl

Higher-order beta-matching

Open mrhaandi opened this issue 10 months ago • 0 comments

  • added higher-order matching wrt. beta-equivalence HOMbeta
  • added reduction from SSTS01 to HOMbeta resulting in undecidable HOMbeta

The reduction is quite different from the known technique by Loader [1]. It is based on the technique used for intersection type inhabitation, see IntersectionTypes/Reductions/SSTS01_to_CD_INH.v, sharing a common seed. A write up for a potential publication is in progress.

[1] Loader, Ralph. "Higher order β-matching is undecidable." Logic Journal of the IGPL 11.1 (2003): 51-68.

mrhaandi avatar Apr 04 '24 10:04 mrhaandi