|Title:||An optimisation of lambda type assignments via resource control||First page:||21||Last page:||22||Conference:||LAP 2015 - Logic and Applications, pp 21-22, September 20-24, 2015, Dubrovnik, Croatia||Issue Date:||2015||Rank:||M34||URL:||http://imft.ftn.uns.ac.rs/math/cms/uploads/Main/LAP2015_book_of_abstracts.pdf||Abstract:||
The size of a lambda term’s type assignment is traditionally interpreted as the number of involved typing rules, since that interpretation corresponds to the complexity of underlying logical proof. However, it can be also assessed using some finer-grained measures such as the number of involved type declarations, or even as the sum of the sizes of all types in involved type declarations. These quantitative properties of type assignments are relevant for implementation issues, e.g. for compiler construction. We propose a type assignment method that relies on the translation of a typeable lambda term to the corresponding term of the resource control lambda calculus. This calculus, introduced by Ghilezan et al. in , contains operators for variable duplication and erasing, and linear substitution, whereas its typed version corresponds to intuitionistic logic with explicit structural rules of contraction and thinning. We prove that the translation preserves the type of a term, and that all output resource control lambda terms are in theirγω-normal forms, meaning that resource control operators are put in optimal positions considering the size of type assignments. The translation output of a given lambda term is often syntactically more complex and therefore more rules need to be used for its type assignment in the target resource control calculus. However, we show that two finer grained measures decrease when types are assigned to terms satisfying a certain minimal level of complexity.
|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
Advanced Techniques of Cryptology, Image Processing and Computational Topology for Information Security
Show full item record
checked on Nov 28, 2022
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.