Semântica Formal

A semântica formal de um comando, de uma expressão ou de um termo λ é o objeto matemático determinado pela sintaxe dessa frase.

Pequenos passos, cláusulas [[·]] e redução β deste tópico — e o julgamento Γ ⊢ e : T no tópico seguinte — partem desse par frase–objeto.

As páginas se agrupam em três blocos. O primeiro avança a configuração ⟨C, σ⟩: atribuição grava no store, if deixa um ramo, while verdadeiro desenrola uma volta; ⇓ nomeia só o store final.

O segundo avalia a árvore pelas cláusulas do construtor. [[e₁ + e₂]] depende só de [[e₁]] e [[e₂]]; ρ interpreta variável e o mesmo ρ entra em toda subexpressão.

O terceiro substitui o argumento no corpo da abstração e testa quando a redução β já parou.

O residual e o σ seguintes após x := v, if ou while estão em Semântica Operacional. Calcular [[3 + 4]] = 7 ou [x + 1], sem listar setas, está em Semântica Denotacional.

σ é peça da configuração e a seta o reescreve. ρ é argumento de [[·]] e não atualiza no meio da expressão: a primeira conta está em Semântica Operacional; a segunda, em Semântica Denotacional.

A seta ⟨C, σ⟩ → ⟨C′, σ′⟩ reescreve comando e memória, em Semântica Operacional. A seta (λx.E) F → E[x := F] reescreve só o termo, em Cálculo lambda.

Decidir se [[e]] = [[e′]] está em Semântica Denotacional. Percorrer o termo à procura de (λ…)(…) e não aplicar λx.E sem o argumento à direita está em Cálculo lambda.