O que é essa notação de estilo "matemática discreta", semelhante a uma fração, usada para regras formais?

18

No artigo "Um tipo de dados JSON replicado sem conflito" , encontrei essa notação para definir formalmente "regras":

Algumas das "regras" mostradas no artigo] [1

Como é chamada essa notação? Como eu o leio?

Por exemplo:

  • a DOCregra não tem nada no seu "numerador" - por que não?
  • as regras EXECe GETparecem ter dois termos separados acima da linha, o que isso significa?
  • a VARregra também se destaca um pouco, pois enquanto muitas outras regras usam algum tipo de flecha (o que eu consideraria "implícito") no topo, essa parece apenas estar dizendo que x é um elemento de alguma coisa.
  • quase tudo é recheado de uma inicial Ap,que o texto descreve como "o estado da réplica p é descrito por Ap, uma função parcial finita" - como um leitor mais experiente dessa notação tenderia a "ver" essa parte de toda regra?

Este site sugeriu uma pergunta relacionada com uma notação de aparência muito parecida, sobre a questão Qual é o significado de ⟨B, s⟩ -> ⟨B ', s'⟩ como regra inicial nesta pergunta sobre pequenos passos semântica? - isso é marcado como semântica operacional e parece ser uma vantagem forte. Essa é realmente a estrutura sob a qual eu deveria interpretar esses números? Você poderia resumir isso facilmente no formulário "curso intensivo" para que, mesmo que eu não consiga verificar a correção de suas provas, eu possa pelo menos entender um pouco mais o que eles estão dizendo nesta seção?

natevw
fonte

Respostas:

25

Esta é uma notação padrão para uma regra de inferência . As premissas são colocadas acima de uma linha horizontal e a conclusão é colocada abaixo da linha. Assim, acaba parecendo uma "fração", mas com uma ou mais proposições lógicas acima da linha e uma única proposição abaixo da linha. Se você vir um rótulo (por exemplo, "LET" ou "VAR" no seu exemplo) ao lado dele, esse é apenas um nome legível por humanos para identificar a regra específica.

Você também pode ver isso como dedução natural ou dedução natural no estilo Gentzen .

Essa é uma notação comum na literatura das linguagens de programação. Você verá isso em todo o lugar. É muito conveniente para os tipos de conclusões e provas estruturadas recursivas que surgem nesse campo.

Você verá essa notação usada para expressar axiomas / regras. Você pode pensar em cada axioma como um modelo com "meta-variáveis" (por exemplo, expr ); você pode substituir cada meta-variável por alguma sintaxe da linguagem de programação (por exemplo, qualquer expressão que seja válida na linguagem de programação) e obterá uma instância da regra. A regra de inferência promete que, se todas as proposições estiverem acima da linha, forem verdadeiras (em alguma instância do modelo, em que você substitui consistentemente cada meta-variável pelo mesmo valor em toda a regra), a proposição abaixo da linha também será verdadeira .

DW
fonte
2
Um uso notável é especificar a inferência do tipo Hindley-Milner: esta resposta para “Que parte de Milner-Hindley você não entende?” Mostra como ler e usar esse conjunto de regras.
DylanSp
Uma pequena correção: as premissas e conclusões são julgamentos , não proposições . As proposições são uma forma específica de julgamento. Nessa linha, os julgamentos são evidentes , não verdadeiros (porque a noção de verdade é difícil de definir e não é realmente interessante para a semântica da linguagem de programação).
precisa saber é o seguinte
7

Aqui está uma explicação muito informal que pode ajudar as pessoas não familiarizadas com as notações formais a entrarem na porta. Não substitui uma definição formal!

O Ap é o estado do seu sistema ou programa em execução. "Estado" pode significar muitas coisas, mas neste caso parece incluir uma lista de todas as variáveis ​​locais definidas e seus valores. Por que Ap é uma função? Por ser uma maneira conveniente de expressar atribuições de variáveis: Ap (x) fornece o valor da variável x .

Agora, vamos tomar a regra EXEC como exemplo. Ele define a semântica de executar um comando cmd1 seguido por um comando cmd2 , ou seja, o que acontece com o estado Ap do sistema ao executar cmd1 seguido de cmd2 .

  • Acima da linha: estas são as instalações. O que eles dizem: "Permita que o cmd1 seja um comando. Se você executar o comando cmd1 quando o sistema estiver no estado Ap , seu sistema terminará em um novo estado Ap ' ."
  • Abaixo da linha: Aqui, a regra descreve o que significa executar dois comandos cmd1 e cmd2 sequencialmente. O que diz: "Supondo que seu sistema esteja no estado Ap , executando cmd1 e cmd2 significa executar cmd2 quando o sistema estiver no estado Ap ' " (lembre-se de que Ap' é o estado que você obtém após executar o cmd1 , conforme definido no instalações).

As outras regras descrevem a semântica dos comandos e expressões individuais. Por exemplo, a regra VAR descreve o que significa "executar" uma variável: se x é uma variável local (acima da linha), o que significa avaliar / executar a variável x ? Está escrito abaixo da linha: Quando o seu programa está no estado Ap , a avaliação de x fornece o valor de x , ou seja, Ap (x) .

Espero que ajude.

porta-malas
fonte
Obrigado, esta é uma grande ajuda para entender e exatamente o que eu estava procurando! No entanto, deixa minha primeira pergunta sem resposta: essa notação tem um nome, geralmente e / ou nesse contexto específico? Meu palpite era "Semântica operacional", mas a outra resposta aqui até agora diz que são apenas "regras de inferência". Eu acho que se eu fizer uma pergunta em duas partes que eu mereço para obter as respostas se separaram, mas agora estou dividido entre qual a aceitar :-)
natevw
1
@natevw São regras de inferência. A semântica operacional é apenas uma das muitas coisas que são comumente expressas com regras de inferência.
Gilles 'SO- stop be evil' (