Sobre Lógica e Programação

Sintaxe e Semântica

Por formal entende-se o tipo de regras, por exemplo, da aritmética ou da sintaxe de programas. Uma expressão aritmética como $$ \large 2 + 3 \times 4 $$ tem uma estrutura que segue um conjunto de definições sintáticas, que determinam o que pode ser escrito.

• Por exemplo $4~3~\times~2~+$ é uma expressão incorreta porque não respeita as definições habituais das expressões aritméticas (porém segue a reversed polish notation).

Por outro lado, o valor resulta de definições semânticas. Por exemplo

• A igualdade $x + y = y + x$ diz que as expressões $x + y$ e $y + x$ têm o mesmo valor.
  • As expressões $x + y$ e $y + x$ são diferentes, porque começam por símbolos diferentes, $x$ e $y$.
  • Mas ambas definem o mesmo valor.
• Outras igualdades deste tipo, como $x + 0 = x$ ou $(x + 1) \times y = x \times y + y$ permitem deduzir, por fim, que $2 + 3 \times 4 = 14$.

• As definições sintáticas especificam o que pode ser escrito, ie as expressões corretas.
• As definições semânticas definem o valor das expressões corretas.

Dedução

Também interessa a noção de dedução: quais são as conclusões de hipóteses dadas?

Em termos práticos:

• Quais são as consequências de certas ações?
  • Se $x = 7$ qual o valor de $x^2 - x$?
• Quais são os meios necessários para um dado objetivo?
  • Qual o valor de $x$ quando $x^2 - x = 42$?

Este interesse vai além da aritmética. Em geral, como é que a estrutura e o valor permitem chegar a conclusões a partir de hipóteses dadas?.

Uma dedução ou prova é uma sequência de passos que começa com hipóteses e termina numa conclusão. Cada um desses passos deve depender apenas das hipóteses e dos passos anteriores, pela aplicação de regras rigorosas.

Hipóteses, passos e conclusão são proposições (ou fórmulas) e as regras definem como certas proposições (ou fórmulas) são conclusão de outras.

A distinção entre estrutura e valor leva a dois tipos de consequência:

• A consequência sintática $H \vdash t$ diz que há uma prova da conclusão $t$ a partir das hipóteses $H$ .
• A consequência semântica $H \models t$ diz que a conclusão $t$ é verdadeira sempre que as hipóteses $H$ são verdadeiras.

No primeiro caso, a consequência sintática, não participam os valores verdade/falso. Só é considerada a estrutura da proposições.

Para a consequência semântica interessam os valores verdade/falso e, também, a estrutura. Por exemplo, usando $\cte{v}$ para verdade e $\cte{f}$ para falso, na tabela

os valores booleanos na coluna $x \lor y$ dependem dos valores $\cte{v}$/$\cte{f}$ de $x$ e de $y$ e também da estrutura de $x \lor y$; a coluna $x \land y$ é diferente porque, embora dependa exatamente dos mesmos valores, tem uma estrutura diferente.

Informática

No caso da informática a descrição e a análise rigorosa de um sistema (ou programa) é fundamental.

Dado o seguinte programa:

#![allow(unused)]
fn main() {
fn answer(x: i32) -> i32  {
    2 * x
}

let y = answer(21);
println!("The answer is {y}.");
}

Os termos usados, como fc, println! ou os parêntesis {, } não são arbitrários; têm de ser exatamente aqueles e não outros. Além disso, a ordem por que são escritos também segue regras precisas. Por exemplo, o fragmento

#![allow(unused)]
fn main() {
answer() {fn} 2 * x i32 i32;
}

é incorreto.

Além das regras de escrita para programas corretos, também é necessário rigor na execução de um programa. O programa acima deve produzir o texto 42 na consola.

Estes dois aspetos dos programas, a escrita (sintaxe) e a execução (semântica), têm de ser definidas rigorosamente num sistema formal.

A lógica é esse sistema, capaz de definir formalmente tanto a sintaxe como a semântica dos programas.

Além de correto, um programa deve ter um comportamento bem definido. Consideremos a seguinte função:

#![allow(unused)]
fn main() {
fn sum(x: i32) -> i32 {
    // x >= 0
    let mut y = 0;
    let mut z = 0;
    while z !== x {
        z = z + 1;
        y = y + z;
    }
    // y = 0 + 1 + ... + x
    y
}
}

Como garantir que o valor devolvido por sum(x) é $y = \sum_{z = 1}^x z$ quando $x \geq 0$?

Uma resposta formal a este problema também permite considerar as seguintes questões:

• Como definir um programa correto?
• Como descrever o comportamento de um programa?
• Como provar que um programa funciona de acordo com as especificações?
• Como desenvolver componentes adicionais?
• Como analizar e tratar situações críticas, de erro, entradas incorretas, etc?
• Como coordenar equipas de dezenas, centenas ou milhares de engenheiros informáticos, com experiências e formações variadas?

Estas questões não podem ser respondidas ad hoc. Precisam de respostas obtidas com rigor e objetividade.

Um sistema informático crítico não pode ter uma estrutura ambígua ou subjetiva; tem de ser descrito objetivamente de forma a que diferentes equipas o possam analizar, utilizar, desenvolver, corrigir, manter, expandir, substituir, etc

Por exemplo, a documentação de uma linguagem, como a rust, de uma biblioteca, como a Distributed, a especificação de um formato, como o yaml, formalizam o que se pode escrever e o respetivo comportamento.