ODIUM
发表于 2025-3-27 00:42:30
Dependency Pairs for Equational Rewritingrary non-collapsing equations (satisfying a certain linearity condition). With the proposed approach, it is now possible to perform automated termination proofs for many systems where this was not possible before. In other words, the power of dependency pairs can now also be used for rewriting modulo equations.
CAB
发表于 2025-3-27 01:28:51
Termination Proofs by Context-Dependent Interpretationsofs by interpretations that can avoid this drawback of the traditional approach. A number of simple examples illustrate how to achieve tight or even optimal bounds on the derivation height. The method is general enough to capture cases where simplification orderings fail.
减去
发表于 2025-3-27 07:50:10
Relating Accumulative and Non-accumulative Functional Programs of functional programs, namely restricted 2-modular tree transducers, to which it can be applied. Moreover, since we get macro tree transducers as transformation result and since we also give the inverse transformation algorithm, we have a new characterization for the class of functions induced by macro tree transducers.
爵士乐
发表于 2025-3-27 10:57:43
http://reply.papertrans.cn/83/8300/829957/829957_34.png
繁忙
发表于 2025-3-27 16:29:17
http://reply.papertrans.cn/83/8300/829957/829957_35.png
脱水
发表于 2025-3-27 20:11:37
http://reply.papertrans.cn/83/8300/829957/829957_36.png
噱头
发表于 2025-3-27 22:06:25
http://reply.papertrans.cn/83/8300/829957/829957_37.png
Omnipotent
发表于 2025-3-28 05:52:08
http://reply.papertrans.cn/83/8300/829957/829957_38.png
Opponent
发表于 2025-3-28 08:34:25
Beta Reduction Constraintsconstraints to describe beta reduction steps between partially known lambda terms. We show that beta reduction constraints can be expressed in an extension of CLLS by group parallelism. We then extend a known semi-decision procedure for CLLS to also deal with group parallelism and thus with beta-red
间接
发表于 2025-3-28 14:25:28
From Higher-Order to First-Order Rewritingof higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty theory (that is, ε = 0). This class includes of course the λ-calculus. Our technique does not rely on a particular substitution calculus but on a set of abstract properties to be verified by the substitut