We use a labelled deduction system ( LNDED−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 LNDEQ−TRS2 rewriting system.
@article{arxiv.2007.07769,
title = {Computational Paths -- An approach in the $LND_{EQ}-TRS_{2}$ system},
author = {Tiago M. L. Veras and Arthur F. Ramos and Ruy J. G. B. de Queiroz and Anjolina G. de Oliveira},
journal= {arXiv preprint arXiv:2007.07769},
year = {2023}
}
Comments
21 pages. arXiv admin note: substantial text overlap with arXiv:1906.09105