进行中的工作：Autosubst 中模式匹配的一种策略
Work-in-Progress: A Tactic for Pattern Matching in Autosubst
浏览论文内容
中文总结 AI 辅助
研究针对 Autosubst 在匹配类型规则等情况时的不足，提出一种进行中的自动模式匹配方法，通过在标准案例研究中评估，为相关匹配问题提供了解决策略。
中文摘要 AI 辅助
Autosubst 能够对无假设等式进行高达西格玛演算的自动等式检查，让用户避免对德布鲁因指标进行繁琐推理。虽在很多情况下有效，但在匹配类型规则、归约关系或引理时不适用，需用户以特定方式表述类型规则或明确替代德布鲁因项，且无贝塔归约时匹配解可能不唯一。本文提出一种针对假设自动模式匹配的进行中的方法，并在包括 POPLMark 和 POPLMark Reloaded 挑战在内的标准案例研究中进行了评估。
英文摘要
Autosubst enables automatic equality-checking up to the sigma-calculus for assumption-free equalities, allowing users to avoid cumbersome reasoning about de Bruijn indices. While effective in many cases, this approach is inapplicable when matching against typing rules, reduction relations, or lemmas, requiring users to either phrase typing rules in a way that they work with Autosubst or even stating explicitly an alternative de Bruijn term. But even without beta-reduction, solutions of matching may not be unique. This paper presents a work-in-progress method for automatically pattern matching against assumptions, evaluated on standard case studies including the POPLMark and POPLMark Reloaded challenges.
