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

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

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?

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 .

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.