


























Abstract:We show that there is a simple syntactically-defined subclass of higher-order benchmarks in the termination problem database for which rewriting according to Nipkow's higher-order rewrite systems (HRSs) and rewriting according to a beta-first strategy in the semantics of TermCOMP's higher-order category coincide. This lays the formal foundation for an HRS (sub)category in TermCOMP which would allow more tools to compete against each other.
From: Johannes Niederhauser [view email]
[v1]
Wed, 24 Jun 2026 06:23:32 UTC (102 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。