Authors: | Ghilezan, Silvia Ivetić, Jelena Lescanne, Pierre Likavec, Silvia |
Title: | Approaching substructural term calculi via the resource control calculus | First page: | 12 | Last page: | 14 | Conference: | LAP 214 - 3rd Conference Logic and Applications, Dubrovnik, 22-26 Septembar | Issue Date: | 2014 | Rank: | M34 | URL: | http://imft.ftn.uns.ac.rs/math/cms/uploads/Main/LAP2014_book_of_abstracts.pdf | Abstract: | In this talk, we propose a new way to obtain a computational interpretation of some substructural logics, starting from an intuitionistic term calculus with explicit control of resources. Substructural logics [1] are a wide family of logics obtained by restricting or rejecting some of Gentzen’s structural rules, such as thinning, contraction and exchange.The most well known substructural logic is the linear logic of Girard [3], in which, due to the absence of contraction and weakening, each formula appears exactly once in the theorem. The other well known substructural logics are the relevant logic (the one without thinning), the affine logic (without contraction) and the Lambek calculus(without all three mentioned structural rules). From the computational point of view, structural rules of thinning and contractionare closely related to the control of available resources (i.e. term variables). More precisely, contraction corresponds to the duplication of the variable that is supposed to be used twice in a term, whereas weakening corresponds to the erasure of an useless variable. These concepts were implemented into several extensions of the lambda calculus [2, 4, 5, 6]. Here, we use the resource control lambda calculus λr, proposed in [2], as a starting point for obtaining computational interpretations of implicative fragments of some substructural logics, namely relevant and affine logic. The corresponding formal calculi are obtained by syntactic restrictions, along with modifications of the reduction rules and the type assignment system. The pre-terms of λr are given by the following abstract syntax: Pre-termsf: =x|λx.f|ff|xf|x |
Project: | Representations of logical structures and formal languages and their application in computing Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education |
Show full item record
Google ScholarTM
Check
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.