Groups and Inverse Semigroups in Lambda Calculus

1. O Problema

O artigo aborda o problema clássico da caracterização dos termos $\lambda$-calculísticos invertíveis módulo diferentes teorias $\lambda$ (relações de equivalência).

• Contexto: Na álgebra do $\lambda$-cálculo, a composição de termos é definida como $M \circ N = \lambda x. M(Nx)$. Um termo $M$ é invertível se existe um $N$ tal que $M \circ N = N \circ M = I$ (o termo identidade).
• Desafio: A natureza dos termos invertíveis depende criticamente da teoria de igualdade considerada:
  • Na teoria mínima ($=\beta$), apenas a identidade $I$ é invertível (grupo trivial).
  • Na teoria extensional ($=\beta\eta$), os termos invertíveis são as Permutações Hereditárias Finitas (FHP).
  • Na teoria observacional máxima ($H^*$), os termos invertíveis são as Permutações Hereditárias (HP), que podem ter árvores de Böhm infinitas.
• Questão Aberta: O artigo visa preencher a lacuna entre essas teorias, especificamente caracterizando os termos invertíveis em teorias intermediárias, como a teoria observacional de Morris ($H^+$), onde a observável é a normalização $\beta$. Uma conjectura de Barendregt sugeriu que, em todas as teorias entre $=\beta\eta$ e $H^+$, os termos invertíveis seriam exatamente os FHPs, mas uma prova formal e unificada faltava.

2. Metodologia

Os autores adotam uma abordagem baseada na Teoria dos Semigrupos Inversos, uma estrutura algébrica que generaliza tanto grupos quanto semilattices.

• Estrutura Algébrica: Em vez de tratar a invertibilidade apenas como uma propriedade de grupo, eles modelam o conjunto de permutações hereditárias como um semigrupo inverso (especificamente, um monóide inverso).
• Objeto de Estudo: Introduzem o conceito de Árvores de Permutação (Permutation Trees - PT). Estas são árvores ordenadas rotuladas com permutações finitas, que correspondem bijectivamente às árvores de Böhm dos termos HP.
• Operações Definidas:
  • Definem uma operação de produto e uma operação unária de "inverso" ($*$) sobre as árvores de permutação, tornando o conjunto $(PT, \cdot, *, \bar{\epsilon})$ um monóide inverso.
  • Estabelecem uma ordem natural ($\leq$) no semigrupo, que corresponde à inclusão de funções parciais injetoras.
• Conexão com $\lambda$-cálculo:
  • Mostram que a ordem natural no monóide de árvores de permutação corresponde à expansão $\eta$ (finita para FHPs e infinita para HPs).
  • Utilizam o conceito de congruência de grupo mínima ($\sigma$), que é a menor congruência que transforma um semigrupo inverso em um grupo (colapsando todos os idempotentes na classe da identidade).

3. Contribuições Principais

O trabalho oferece uma reconstrução conceitual unificada e novos resultados sobre a invertibilidade:

1. Estrutura de Semigrupo Inverso: Demonstram que o conjunto de permutações hereditárias (HP) módulo a teoria das árvores de Böhm, e o conjunto de permutações hereditárias finitas (FHP) módulo $=\beta$, formam monóides inversos F-inversos (uma classe específica onde cada classe de equivalência tem um único elemento maximal).
2. Correspondência com Expansão $\eta$: Provaram que a ordem natural do semigrupo inverso coincide exatamente com a pré-ordem induzida pela expansão $\eta$:
   • Para FHPs: Ordem natural $\leftrightarrow$ expansão $\eta$ finita.
   • Para HPs: Ordem natural $\leftrightarrow$ expansão $\eta$ infinita.
3. Reconstrução de $H^*$ e $=\beta\eta$: Mostram que as teorias $H^*$ e $=\beta\eta$ surgem naturalmente como o resultado de quocientar os monóides inversos pela congruência de grupo mínima ($\sigma$). Isso fornece uma nova perspectiva algébrica para a caracterização clássica de Dezani-Ciancaglini, Bergstra e Klop.
4. Resolução da Conjectura de Barendregt: O resultado central é a prova de que, para qualquer teoria $\lambda$ $T$ tal que $=\beta\eta \subseteq T \subseteq H^+$, o conjunto de termos invertíveis é exatamente o conjunto FHP.
   • Isso resolve a conjectura de que a "barreira" para a invertibilidade infinita (HPs) só é quebrada na teoria $H^*$, e não em teorias intermediárias como $H^+$.

4. Resultados Técnicos Chave

• Teorema 49: Um termo $M$ é invertível na teoria $H^+$ se e somente se $M$ é uma Permutação Hereditária Finita (FHP).
• Teorema 39 e 48: Estabelecem a equivalência entre a igualdade na teoria ($H^*$ ou $H^+$) e a igualdade dos elementos maximais das classes de congruência $\sigma$ (ou $\sigma'$) no monóide de árvores de permutação.
  • Em $H^*$: $M =_{H^*} N \iff BT(M)^m = BT(N)^m$ (onde $m$ é a operação de tomar o elemento maximal).
  • Em $H^+$: $M =_{H^+} N \iff BT(M)^{m'} = BT(N)^{m'}$ (usando uma ordem e congruência adaptadas para expansões finitas).
• Propriedade F-inversa: A prova de que o monóide de árvores de permutação é F-inverso é crucial, pois garante que os elementos maximais formam um grupo isomorfo ao grupo de unidades do quociente pelo grupo mínimo.

5. Significado e Impacto

• Unificação Algébrica: O trabalho demonstra que a teoria dos semigrupos inversos é a estrutura natural para estudar a invertibilidade no $\lambda$-cálculo, unificando casos finitos e infinitos sob uma mesma ótica algébrica.
• Clarificação de Teorias Intermediárias: Ao provar que $H^+$ ainda mantém os FHPs como únicos invertíveis, o artigo delimita com precisão onde a complexidade da invertibilidade muda (somente em $H^*$ e teorias superiores).
• Ferramentas para Futura Pesquisa: A introdução das árvores de permutação e a análise da interação entre idempotentes infinitos e ordens finitas abrem caminho para investigar teorias entre $H^+$ e $H^*$, onde os autores conjecturam que podem existir grupos de invertíveis estritamente intermediários entre FHP e HP.
• Relevância para Semântica: Reforça a conexão entre propriedades operacionais (como normalização e árvores de Böhm) e estruturas algébricas abstratas, oferecendo novas ferramentas para a análise de modelos denotacionais e semânticas de jogos.

Em suma, o artigo transforma um problema de caracterização de termos em um problema de estrutura de semigrupos, fornecendo provas elegantes e definitivas para conjecturas antigas sobre a natureza da invertibilidade no $\lambda$-cálculo.