Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/756
Título: | Encoding linear logic with interaction combinators |
Autor(es): | Mackie, Ian Pinto, Jorge Sousa |
Palavras-chave: | Interaction nets Linear logic Cut-elimination Lambda-calculus cut-elimation ?-calculus |
Data: | Ago-2002 |
Editora: | Elsevier Science |
Revista: | Information and Computation |
Citação: | “Information and Computation”. ISSN 0890-5401.176:2 (2002) 153-186. |
Resumo(s): | The purpose of this paper is to demonstrate how Lafont’s interaction combinators, a system of three symbols and six interaction rules, can be used to encode linear logic. Specifically, we give a translation of the multiplicative, exponential and additive fragments of linear logic together with a strategy for cut-elimination which can be faithfully simulated. Finally, we show briefly how this encoding can be used for evaluating (...)-terms. In addition to offering a very simple, perhaps the simplest, system of rewriting for linear logic and the (...)-calculus, the interaction net implementation that we present has been shown by experimental testing to offer a good level of sharing, in terms of the number of cut-elimination steps (resp. (...)-reduction steps). In particular it performs better than all extant finite systems of interaction nets. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/756 |
DOI: | 10.1006/inco.2002.3163 |
ISSN: | 0890-5401 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
mackie-pinto.pdf | 2,89 MB | Adobe PDF | Ver/Abrir |