2018/09/12 by Arthan, Rob, Oliva, Paulo
#03B15 #03B20 #03B40 #03B47 #03B50 #03B70 #03F52 #68N18 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1809.04492
In this paper we introduce a term calculus \cal B which adds to the affine λ-calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a Curry-Howard correspondence between \cal B and the sub-structural logical system which we call "minimal Ł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 \cal B is strongly normalising and has the Church-Rosser property. We also give examples of terms in \cal 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 Łukasiewicz logic.