Multiset path order improved for partial and variable function use
An Applicative Multiset Path Order (Extended Version)
Logic in Computer Science
Summary
When computers check if one program step comes before another, they often need special rules. The authors created a new set of rules to handle tricky cases where functions don't get all inputs or are given variable parts. Their method uses two new ideas called arity assignment and reification to solve these problems. This helps make sure the steps follow the right order even in complicated programs.
What this means in practice
- •For programming language designers: Use the improved path order to better handle partial and variable function applications in language semantics and optimization.
- •For automated theorem prover developers: Incorporate the variant to enhance termination checking in theorem provers dealing with untyped applicative term rewriting systems.
A theory result. No direct application yet.
Authors
Nao Hirokawa, Teppei Saito, Teppei Tanaka, Wataru Yachi
Abstract
We present a variant of the multiset path order for untyped applicative term rewriting. Compared to existing work, our variant incorporates two distinctive features, dubbed arity assignment and reification, to overcome difficulties in handling partial and variable application.