Authors: Ghilezan, Silvia Ivetić, JelenaLescanne, PierreLikavec, 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 where x ranges over a denumerable set of term variables, λx.f is an abstraction,ff is an application, xf is a thinning and 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

#### Page view(s)

64
checked on May 9, 2024