A Curry-Howard Correspondence for the Minimal Fragment of {\L}ukasiewicz Logic

In this paper we introduce a term calculus $\mathcal{B}$ which adds to the affine $\lambda$-calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a Curry-Howard correspondence between $\mathcal{B}$ and the sub-structural logical system which we call “minimal {\L}ukasiewicz logic”, also known in the literature as the logic of hoops (a generalisation of MV-algebras). This logic lies strictly in between affine minimal logic and standard minimal logic. We prove that $\mathcal{B}$ is strongly normalising and has the Church-Rosser property. We also give examples of terms in $\mathcal{B}$ corresponding to some important derivations from our work and the literature. Finally, we discuss the relation between normalisation in ${\cal B}$ and cut-elimination for a Gentzen-style formulation of minimal {\L}ukasiewicz logic.