Semântica Operacional

A semântica operacional define o significado de um programa especificando como ele é executado, usando regras de inferência que descrevem os passos da computação.

Definition

A semântica operacional especifica o significado de um programa como a sequência de passos de computação que ele executa, dada por relações de transição definidas indutivamente sobre configurações de programa.

Scope

Este tópico abrange a semântica operacional de pequeno passo (estrutural) e de grande passo (natural), nas quais as relações de transição ou avaliação definidas por regras de inferência direcionadas pela sintaxe descrevem como os programas computam. Aborda estratégias de redução, máquinas abstratas e como as definições operacionais apoiam provas de correção de tipos e equivalência de programas.

Core questions

• Como as regras de inferência capturam os passos de uma computação?
• Qual a diferença entre semântica de pequeno passo e de grande passo?
• Como a semântica operacional apoia provas de correção e equivalência?
• Como as máquinas abstratas se relacionam com as definições operacionais baseadas em regras?

Key theories

Semântica operacional estrutural

Plotkin define a execução por regras de transição de pequeno passo estruturadas pela sintaxe da linguagem, fornecendo uma descrição composicional e direcionada pela sintaxe de como cada construção computa.

Semântica natural (de grande passo)

A semântica natural de Kahn relaciona um programa diretamente ao seu resultado final através de regras de avaliação, abstraindo os passos intermediários e facilitando certas provas.

Clinical relevance

A semântica operacional é a ferramenta padrão para especificar o comportamento de linguagens reais e provar a correção de compiladores e interpretadores. Seu estilo baseado em regras se alinha estreitamente com as implementações e fundamenta a metateoria de linguagens verificada por máquina.

History

Ideias operacionais surgiram nas primeiras definições de linguagens baseadas em interpretadores. As notas de Aarhus de Plotkin de 1981 estabeleceram a semântica operacional estrutural como uma estrutura rigorosa e direcionada pela sintaxe, e a semântica natural de Kahn de 1987 ofereceu uma alternativa de grande passo. Juntas, elas se tornaram a abordagem dominante para definir e raciocinar sobre linguagens de programação.

Debates

Formulações de pequeno passo versus grande passo

Os semanticistas escolhem entre a semântica de pequeno passo, que expõe estados intermediários e lida naturalmente com não-terminação e concorrência, e a semântica de grande passo, que é concisa, mas menos adequada para computações divergentes ou intercaladas.

Key figures

• Gordon Plotkin
• Gilles Kahn
• Glynn Winskel
• Matthias Felleisen

Seminal works

• plotkin1981
• kahn1987
• winskel1993

Frequently asked questions

Qual a diferença entre semântica de pequeno passo e de grande passo?

A semântica de pequeno passo descreve os passos de computação individuais e os estados intermediários entre eles, enquanto a semântica de grande passo relaciona um programa diretamente ao seu valor final, ocultando os passos intermediários.

Por que a semântica operacional é útil para provar a correção?

Como ela torna explícitos os passos da execução, ela se associa naturalmente ao método de progresso e preservação, que raciocina sobre como a tipagem é mantida à medida que um programa executa cada passo.