Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/13192
Título: | A calculus of multiary sequent terms |
Autor(es): | Espírito Santo, José Pinto, Luís F. |
Palavras-chave: | Intuitionistic sequent calculus Lambda calculus Curry-Howard isomorphism Generalized application Multiary application Permutative conversions Languages Theory |
Data: | Mai-2011 |
Editora: | ACM |
Revista: | ACM Transactions on Computational Logic |
Resumo(s): | Multiary sequent terms were originally introduced as a tool for proving termination of permutative conversions in cut-free sequent calculus. This work develops the language of multiary sequent terms into a term calculus for the computational (Curry-Howard) interpretation of a fragment of sequent calculus with cuts and cut-elimination rules. The system, named generalised multiary lambda-calculus, is a rich extension of the lambda-calculus where the computational content of the sequent calculus format is explained through an enlarged form of the application constructor. Such constructor exhibits the features of multiarity (the ability of forming lists of arguments) and generality (the ability of prescribing a kind of continuation). The system integrates in a modular way the multiary lambda-calculus and an isomorphic copy of the lambda-calculus with generalised application LambdaJ (in particular, natural deduction is captured internally up to isomorphism). In addition, the system: (i) comes with permutative conversion rules, whose role is to eliminate the new features of application; (ii) is equipped with reduction rules --- either the mu-rule, typical of the multiary setting, or rules for cut-elimination, which enlarge the ordinary beta-rule. This paper establishes the meta-theory of the system, with emphasis on the role of the mu-rule, and including a study of the interaction of reduction and permutative conversions. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/13192 |
DOI: | 10.1145/1929954.1929959 |
ISSN: | 1529-3785 |
Versão da editora: | http://portal.acm.org/ |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
lambda-for-seq(RepositoriUM).pdf | 638,04 kB | Adobe PDF | Ver/Abrir |