论文标题
计算路径 - $ lnd_ {eq} -trs_ {2} $ system中的一种方法
Computational Paths -- An approach in the $LND_{EQ}-TRS_{2}$ system
论文作者
论文摘要
我们根据计算路径（重写的序列）的概念使用标记的扣除系统（LND $ _ {ED - } $ TRS）作为相同类型的两个术语之间的平等性，这使我们可以使用计算路径的概念在同型理论中执行一种方法。由此，我们表明计算路径可用于执行$ lnd_ {eq} -trs_ {2} $重写系统的证明。
We use a labelled deduction system ( LND$_{ED-}$TRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which allowed us to carry out in homotopic theory an approach using the concept of computational paths. From this, we show that the computational paths can be used to perform the proofs of the $LND_{EQ}-TRS_{2}$ rewriting system.
