We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. We show that any transfinite reduction can be faithfully represented as an infinitary proof term, which is unique up to, infinitary, associativity.
Our main use of proof terms is in a definition of permutation equivalence for transfinite reductions, on the basis of permutation equations. This definition involves a variant of equational logic, adapted for dealing with infinite objects.
A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.
We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (Extended Version)
我们提出了一个共归纳的框架，定义无穷类似物的方程推理和重写统一的方式。我们定义关系=^infty，无限等式推理的概念，和->^infty，无限重写的标准概念如下：=^infty：= nu R。（<-_root + ->_root + lift（R））^* ->^infty：= mu R. nu S（->_root + lift（R））^* ; lift（S）其中lift（R）：= {（f（s_1，.，s_n），f（t_1，.，t_n））|s_1 R t_1，.，s_n R t_n } + id，其中mu是最小不动点算子，nu是最大不动点算子.该设置捕获任意序数长度的重写序列，但它既不需要序数也不需要度量收敛。这使得该框架特别适合于定理证明器中的形式化。
Proof terms in term rewriting are a representation means for reduction sequences, and more in general for contraction activity, allowing to distinguish e.g simultaneous from sequential reduction. Proof terms for finitary, first-order, left-linear term rewriting are described in the Terese book, chapter 8. In a previous work, we defined an extension of the finitary proof-term formalism, that allows to describe contractions in infinitary first-order term rewriting, and gave a characterisation of permutation equivalence. In this work, we discuss how projections of possibly infinite rewrite sequen…
The Size-Change Termination principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a system of dependent types extending LF.
We introduce an infinitary first order linear logic with least and greatest fixed points. To ensure cut elimination, we impose a validity condition on infinite derivations. Our calculus is designed to reason about rich signatures of mutually defined inductive and coinductive linear predicates. In a major case study we use it to prove the strong progress property for binary session-typed processes under an asynchronous communication semantics. As far as we are aware, this is the first proof of this property.
Monads can be interpreted as encoding formal expressions, or formal operations in the sense of universal algebra. We give a construction which formalizes the idea of "evaluating an expression partially": for example, "2+3" can be obtained as a partial evaluation of "2+2+1". This construction can be given for any monad, and it is linked to the famous bar construction, of which it gives an operational interpretation: the bar construction induces a simplicial set, and its 1-cells are partial evaluations. We study the properties of partial evaluations for general monads. We prove that whenever the…
