skip to main content
Idioma:
Primo Search
Clear Search Box
Search in: Busca Geral
Busca Avançada
Busca por Índices

Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Dowek, Gilles ; Férey, Gaspard ; Jouannaud, Jean-Pierre ; Liu, Jiaxiang

Mathematical structures in computer science, 2022-08, Vol.32 (7), p.898-933 [Periódico revisado por pares]

Cambridge, UK: Cambridge University Press

Texto completo disponível

Citações Citado por
  • Título:
    Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs
  • Autor: Dowek, Gilles ; Férey, Gaspard ; Jouannaud, Jean-Pierre ; Liu, Jiaxiang
  • Assuntos: Calculus ; Computer Science ; Logic in Computer Science ; Special Issue: Confluence ; Syntax ; Variables
  • É parte de: Mathematical structures in computer science, 2022-08, Vol.32 (7), p.898-933
  • Descrição: User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom’s decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, confluence of a terminating set of left-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. The present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pairs. The rewrite relation used for analyzing confluence may rewrite arbitrarily many non-overlapping redexes in a single step. This relation gives rise to critical pairs that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. Practical examples of use of this technique are analyzed.
  • Editor: Cambridge, UK: Cambridge University Press
  • Idioma: Inglês
Links
Voltar para lista de resultados

  • Realização: ABCD-USP USP   Logos de Redes Sociais: Freepik

Buscando em bases de dados remotas. Favor aguardar.