💻 computer science

Fully Evaluated Left-Sequential Logics

Este artigo introduz uma hierarquia de lógicas sequenciais à esquerda totalmente avaliadas, que vai da FEL Livre até a FEL Estática, fornecendo axiomatizações completas para suas versões de dois e três valores, utilizando árvores de avaliação como fundamento semântico.

Autores originais: Alban Ponse, Daan J. C. Staudt

Publicado 2026-05-14

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Alban Ponse, Daan J. C. Staudt

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você é um chef preparando um prato complexo. No mundo da lógica computacional, os "ingredientes" são fatos (verdadeiros ou falsos), e as "receitas" são instruções sobre como combiná-los. Este artigo apresenta uma família de estilos culinários chamados Lógicas Left-Sequential Avaliadas Completamente (FELs).

A ideia central é simples: Você deve provar cada ingrediente individualmente, em ordem, da esquerda para a direita, antes de decidir se o prato está pronto. Você não pode pular uma etapa e não pode parar no meio do caminho apenas porque o primeiro ingrediente tinha gosto ruim.

Aqui está uma análise dos diferentes "estilos culinários" (lógicas) que os autores exploram, usando analogias do cotidiano.

1. A Regra Básica: "Left-Sequential"

Nestas lógicas, a ordem importa. Se você tem uma receita A então B, você deve provar A primeiro.

O Ponto: Os autores usam um ponto especial (como ∧•) para mostrar isso. Significa "Prove o lado esquerdo primeiro. Assim que isso estiver feito, prove o lado direito."
A Diferença: Na lógica normal (como uma tabela-verdade padrão), se a primeira parte for "Falsa", você pode parar ali porque a coisa toda já é falsa. Nestas lógicas, você continua. Você prova a segunda parte de qualquer maneira. Isso é chamado de "Avaliação Completa".

2. Os Quatro Níveis de "Estilos Culinários"

O artigo apresenta uma hierarquia de quatro lógicas, variando da mais caótica à mais rígida. Pense nelas como diferentes níveis de disciplina na cozinha.

Nível 1: FEL Livre (FFEL) – O "Degustador Caótico"

O Vibe: Este é o estilo mais básico, "livre".
A Regra: Você prova tudo em ordem. No entanto, se você provar o mesmo ingrediente duas vezes (por exemplo, A e depois A novamente), a segunda vez pode ter um gosto diferente porque a primeira vez mudou a cozinha!
A Analogia: Imagine provar um limão. A primeira vez, é azedo. Mas se você provar novamente imediatamente após espremê-lo, talvez agora seja apenas uma casca molhada. No FFEL, A e A não são necessariamente iguais porque o primeiro A pode ter tido um "efeito colateral" (como mudar o ambiente).
Característica Chave: É imune a efeitos colaterais apenas se você prometer que os ingredientes não mudam. É a lógica "mais fraca" porque permite a maior imprevisibilidade.

Nível 2: FEL Memorizante (MFEL) – O "Chef que Anota"

O Vibe: Este chef é organizado.
A Regra: Se você provar um ingrediente (digamos, A), você o anota em um caderno. Se encontrar A novamente mais tarde na receita, você apenas olha no seu caderno. Você não prova novamente.
A Analogia: Imagine um guarda de segurança verificando identidades. Se ele verifica seu documento na porta, ele não precisa verificar novamente na entrada dos fundos; ele se lembra de você.
Característica Chave: Isso remove os "efeitos colaterais". Uma vez que um átomo (ingrediente) é avaliado, seu valor é fixo para o resto do processo. Isso torna a lógica mais forte e previsível.

Nível 3: FEL Condicional (CℓFEL) – A "Equipe Flexível"

O Vibe: Esta equipe pode trocar de lugar.
A Regra: É como o MFEL (você lembra o que provou), mas agora você pode trocar a ordem dos ingredientes se eles forem diferentes. A então B é tratado da mesma forma que B então A.
A Analogia: Imagine um grupo de amigos decidindo onde comer. Se Alice e Bob estão decidindo entre Pizza e Sushi, não importa quem fala primeiro; a decisão final é a mesma.
Característica Chave: Esta lógica é equivalente a uma famosa lógica de três valores chamada Lógica de Bochvar. Ela lida com ingredientes "indefinidos" (como um ovo quebrado) tratando o prato inteiro como "quebrado" (indefinido) imediatamente.

Nível 4: FEL Estática (SFEL) – O "Contador Rigoroso"

O Vibe: O estilo mais rígido e tradicional.
A Regra: Esta é apenas a lógica proposicional padrão (como matemática do ensino médio), mas com a regra de que você ainda prova tudo em ordem.
A Analogia: Este é o "Padrão Ouro". Se você tem uma receita que diz "Se o ovo estiver ruim, o bolo está ruim", esta lógica concorda. Ela absorve todo o caos.
Característica Chave: É tão rigorosa que não consegue lidar com ingredientes "indefinidos". Se você tentar misturar "indefinido" com "falso", a matemática quebra (porque Indefinido se torna Falso, o que é uma contradição).

3. O Ingrediente "Indefinido" (U)

Os autores também exploram o que acontece se um ingrediente for Indefinido (U).

Nos estilos "Livre" e "Memorizante": Se você provar um ingrediente indefinido, todo o processo para ou se torna indefinido. É como tentar assar um bolo com "pó misterioso". O resultado é "bolo misterioso".
A Regra "Absorvente": Na versão mais forte de três valores (FEL Condicional), o ingrediente indefinido é "absorvente". Se você misturar Indefinido com qualquer coisa, o resultado é Indefinido. É como um buraco negro na sua receita.

4. As "Árvores" da Lógica

Para provar que suas regras funcionam, os autores usam Árvores de Avaliação.

Imagine uma Árvore Genealógica:
- O topo é a pergunta principal.
- Os galhos são os caminhos "Esquerda" (Verdadeiro) e "Direita" (Falso).
- As folhas na parte inferior são as respostas finais (Verdadeiro ou Falso).
A Inovação: Nestas lógicas, a árvore mostra o caminho exato que você percorreu. Se você provou A, depois B, a árvore mostra essa jornada específica. Na lógica "Memorizante", a árvore é mais limpa porque não mostra você provando o mesmo ingrediente duas vezes.

Resumo da Conquista do Artigo

Os autores não apenas descreveram esses estilos culinários; eles escreveram os Regulamentos (Axiomas) para cada um.

Eles definiram exatamente como combinar ingredientes (equações).
Eles provaram que esses regulamentos são Completos (cobrem todos os cenários possíveis) e Independentes (nenhuma regra é redundante; você não pode remover nenhuma sem quebrar o sistema).
Eles usaram ferramentas computacionais (Prover9 e Mace4) para verificar sua matemática duas vezes, garantindo que nenhum erro humano tivesse passado.

Em resumo: Este artigo mapeia um espectro de sistemas lógicos onde você é forçado a provar cada ingrediente individualmente em ordem. Começa com um sistema caótico onde os ingredientes podem mudar, passa para um sistema onde você lembra o que provou, depois para um sistema onde a ordem não importa e, finalmente, para um sistema rígido que se comporta como matemática padrão. Eles fornecem as leis matemáticas exatas para cada estilo.

Resumo Técnico: Lógicas Left-Sequential Totalmente Avaliadas

Enunciado do Problema
Este artigo aborda a formalização e axiomatização das "Lógicas Left-Sequential Totalmente Avaliadas" (FELs). Diferentemente das lógicas de curto-circuito (SCLs), onde a avaliação cessa assim que o resultado de uma expressão composta é determinado, as FELs prescrevem uma estratégia de avaliação "total" ou "estrita": cada proposição atômica dentro de um termo é avaliada, independentemente de seu valor ser estritamente necessário para o resultado final. Essa estratégia é motivada por contextos de programação onde efeitos colaterais (por exemplo, alterações de estado) devem ser garantidos para ocorrer em todos os átomos de uma expressão. Os autores visam definir uma hierarquia de tais lógicas, variando da mais fraca (FEL Livre), que é imune a efeitos colaterais atômicos, até a mais forte (FEL Estática), que se comporta como uma versão sequencial da lógica proposicional clássica. Além disso, o artigo estende essas lógicas para um cenário de três valores para lidar com a "indefinição" ( $U$ ), uma característica comum em programação e lógica (por exemplo, divisão por zero).

Metodologia
Os autores empregam um quadro semântico baseado em árvores de avaliação, um conceito introduzido em seu trabalho anterior [19].

Semântica: As árvores de avaliação são árvores binárias onde os nós internos representam átomos e as folhas representam valores de verdade ( $T$ $T$ , $F$ $F$ ou $U$ $U$ ). Um caminho da raiz à folha modela uma sequência de avaliação.
- Na FEL Livre (FFEL), a estrutura da árvore preserva estritamente a ordem de avaliação e permite ocorrências repetidas do mesmo átomo, modelando potenciais efeitos colaterais.
- Na FEL Memorizante (MFEL), a semântica é refinada de modo que nenhum caminho na árvore contenha múltiplas ocorrências do mesmo átomo; a avaliação de um átomo é "memorizada" se encontrada novamente.
- Na FEL Condicional (CℓFEL), a lógica incorpora a comutatividade dos átomos, tratando efetivamente a ordem de átomos independentes como irrelevante.
- Na FEL Estática (SFEL), a lógica colapsa para uma versão sequencial da lógica proposicional onde as leis de absorção valem.
Extensão de Três Valores: Para todas as lógicas exceto a SFEL, os autores introduzem uma constante $U$ (indefinido). A semântica é estendida para árvores com folhas em $\{T, F, U\}$ , onde $U$ atua como um elemento absorvente (por exemplo, $U \land_r x = U$ ).
Axiomatização: A principal contribuição metodológica é a derivação de axiomatizações equacionais completas para cada lógica. Os autores definem formas normais (por exemplo, Forma Normal FEL, formas $\sigma$ -normais) para provar a completude. Eles utilizam o provador de teoremas Prover9 para verificar derivabilidades e o Mace4 para gerar contra-modelos finitos para provar a independência dos axiomas.

Principais Contribuições e Resultados

Hierarquia de FELs de Dois Valores:
- FEL Livre (FFEL): A lógica mais fraca, axiomatizada pelo conjunto $EqFFEL$. Ela refuta a idempotência ( $x \land_r x \neq x$ ) mas satisfaz a associatividade. É a lógica da avaliação total sem restrições de efeitos colaterais.
- FEL Memorizante (MFEL): Axiomatizada pela adição de um axioma à FFEL (especificamente, $(x \lor_r y) \land_r z = (\neg x \land_r (y \land_r z)) \lor_r (x \land_r z)$ ). Ela impõe que átomos repetidos sejam tratados como idênticos, eliminando efeitos colaterais.
- FEL Condicional (CℓFEL $_2$ ): Axiomatizada pela adição da comutatividade ( $x \land_r y = y \land_r x$ ) à MFEL. Esta lógica é equivalente à sublógica de dois valores da Lógica Condicional (Guzmán e Squier [12]).
- FEL Estática (SFEL): A lógica mais forte, obtida pela adição de $x \land_r F = F$ à CℓFEL $_2$ . É equivalente à Lógica de Curto-Circuito Estática (SSCL) e à lógica proposicional padrão sob avaliação sequencial.
Extensões de Três Valores (FELU):
- Os autores definem versões de três valores (FFELU, MFELU, CℓFEL) adicionando os axiomas $\neg U = U$ e $U \land_r x = U$ .
- CℓFEL (a FEL Condicional de três valores) é provada ser equivalente à lógica estrita de Bochvar [8].
- SFEL não pode ser estendida com $U$ porque a lei de absorção $F = U \land_r F = U$ leva a um colapso dos valores de verdade.
Completude e Independência:
- Axiomatizações equacionais completas são fornecidas para todas as lógicas definidas.
- Os autores apresentam conjuntos alternativos e mais concisos de axiomas independentes para cada lógica (por exemplo, o conjunto $MF$ para MFEL), verificados usando ferramentas automatizadas.
- Formas normais são construídas para provar que a igualdade sintática das formas normais corresponde à igualdade semântica das árvores de avaliação.

Significado e Alegações
O artigo alega fornecer um quadro unificado para entender a avaliação left-sequential total, preenchendo a lacuna entre as lógicas de curto-circuito e a lógica proposicional clássica.

Previsibilidade: Os autores argumentam que as FELs oferecem maior previsibilidade quanto ao estado do ambiente (efeitos colaterais) após a avaliação em comparação com as SCLs, pois todos os átomos são garantidos de serem avaliados.
Expressividade: O artigo demonstra que, embora a FFEL não possa expressar certas árvores de avaliação uniformes (por exemplo, árvores onde um átomo aparece em ramos diferentes com resultados diferentes), a MFEL e lógicas mais fortes podem expressar essas árvores, aumentando assim o poder expressivo da lógica.
Relação com Trabalhos Existentes: O trabalho situa a CℓFEL dentro da hierarquia de lógicas, mostrando que é equivalente à lógica de Bochvar e uma sublógica da Lógica Condicional. Também esclarece a relação entre FELs e Lógicas de Curto-Circuito (SCLs), notando que os conectivos FEL podem ser definidos dentro de quadros SCL (e vice-versa sob condições específicas), embora as FELs imponham uma disciplina de avaliação mais estrita.

O artigo conclui que essas lógicas fornecem uma base teórica robusta para o raciocínio sobre expressões onde a avaliação total é necessária, oferecendo axiomatizações completas e independentes que facilitam o raciocínio e a verificação automatizados.