Lógica e Computação

A Lógica proporciona um enquadramento formal para descrever e analizar com rigor um determinado assunto.

O objetivo principal deste texto é apresentar a Lógica como uma ferramenta para a descrição e análise de sistemas informáticos.

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 $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 $43 \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 ⊢ t$ diz que há uma prova da conclusão $t$ a partir das hipóteses $H$ .

A consequência semântica $H ⊨ 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 $v$ para verdade e $f$ para falso, na tabela

$x$	$y$	$x \lor y$	$x \land y$
$v$	$v$	$v$	$v$
$v$	$f$	$v$	$f$
$f$	$v$	$v$	$f$
$f$	$f$	$f$	$f$

os valores booleanos na coluna $x \lor y$ dependem dos valores $v$ / $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.

Esquema de Programa

Para concretizar o objetivo deste curso o programa segue os seguintes assuntos:

A lógica proposicional é relativamente simples e flexível para descrever alguns domínios simples. No entanto tem limitações que limitam o seu uso em casos reais.
A lógica de primeira ordem é significativamente mais expressiva e resolve muitas das limitações da lógica proposicional. Essa expressividade vem à custa de alguma complexidade e limites computacionais.
A verificação de programas ilustra uma aplicação da lógica à informática:
- Dada a especificação formal do comportamento de um programa, como deduzir com rigor que o programa funciona como pretendido?