Computational Paths -- An approach in the $LND_{EQ}-TRS_{2}$ system

TL;DR

This paper introduces a labelled deduction system based on computational paths, enabling homotopic reasoning and proof construction within the $LND_{EQ}-TRS_{2}$ rewriting framework.

Contribution

It presents a novel application of computational paths in a labelled deduction system for homotopic theory and rewriting systems.

Findings

Computational paths can be used to perform proofs in the $LND_{EQ}-TRS_{2}$ system.

The approach bridges homotopic theory with rewriting systems.

The system facilitates formal reasoning using sequences of rewrites as equalities.

Abstract

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.