Números

Os tipos que definimos até agora são exemplos de tipos enumerados: suas definições enumeram explicitamente um conjunto finito de elemento. Um jeito mais interessante de definir um tipo é estabelecer uma coleção de regras indutivas descrevendo seus elementos. Por exemplo, nós podemos definir os números naturais da seguinte maneira:

type Nat {
  zero
  succ (pred: Nat)
}

Essa definição pode ser lida como:

• Nat.zero é um número natural;
• Nat.succ é um construtor que recebe um número natural, construindo outro número natural;
  • Ou seja, se n é um número natural, então (Nat.succ n) também será.

Todo tipo definido indutivamente (Como Nat, Bool ou Dia) é um conjunto de expressões. A definição de Nat diz como expressões do tipo Nat podem ser construídas:

• A expressão Nat.zero pertence ao conjunto dos Nat;
• Se n é uma expressão do conjunto dos Nat, então (Nat.succ n) também é uma expressão do conjunto dos Nat; e
• Expressões formadas dessas duas formas são as únicas que pertencem à Nat.

As mesmas regras se aplicam para nossas definições de Dia e Bool. As anotações que usamos para eles são análogas à do construtor Nat.zero, indicando que não recebem nenhum argumento.

Essas três condições demonstram o poder das declarações indutivas. Elas implicam que a expressão Nat.zero, a expressão (Nat.succ Nat.zero), a expressão (Nat.succ (Nat.succ Nat.zero)) e assim por diante, são do conjunto Nat, enquanto outras expressões como Bool.true, (Andb Bool.true Bool.false), e (Nat.succ (Nat.succ Bool.false)) não são.

Nós podemos escrever funções simples usando pattern matching em números naturais da mesma forma que fizemos acima - por exemplo, a função predecessor:

Pred (n: Nat) : Nat
// Como números naturais são estritamente não-negativos,
// usamos como convenção que qualquer coisa que seria
// menor do que 0 retorna 0
Pred  Nat.zero    = Nat.zero
Pred (Nat.succ k) = k

O segundo pattern pode ser lido como: "se n tem a forma (Nat.succ k) para algum k, retorne k."

MinusTwo (n: Nat) : Nat
MinusTwo  Nat.zero               = Nat.zero
MinusTwo (Nat.succ  Nat.zero)    = Nat.zero
MinusTwo (Nat.succ (Nat.succ k)) = k

Para evitar ter que escrever uma sequência de Nat.succ toda vez que você quiser um Nat, é possível usar sufixo n ao final de número qualquer, exemplo o5n, que recebe um número escrito no tipo primitivo U60 mais o sufixo n e retorna o Nat correspondente. {...}

Test : Equal Nat 6n (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))
Test = Equal.refl

O construtor Nat.succ tem tipo Nat -> Nat, assim como as funções MinusTwo e Pred. Todos eles são coisas que, ao serem aplicadas a um Nat, retornam um Nat. A diferença essencial entre o Nat.succ e os outros dois, no entanto, é que funções vem com regras de redução - por exemplo, Pred (Nat.succ Nat.zero) é reduzível para Nat.zero - enquanto que o Nat.succ não. Apesar de ele ser uma função aplicável a um argumento, ela não computa nada.

Para a maioria das definições de funções de números, só pattern matching não é suficiente: nós precisaremos também de recursão. Por exemplo, para checar que um número n é par, nós podemos checar recursivamente se n-2 é par.

Evenb (n: Nat) : Bool
Evenb  Nat.zero               = Bool.true
Evenb (Nat.succ  Nat.zero)    = Bool.false
Evenb (Nat.succ (Nat.succ k)) = Evenb k

Nós podemos definir Oddb (função para checar se um número é ímpar) com uma declaração recursiva semelhante, mas também temos uma definição mais simples e um pouco mais fácil de trabalhar:

Oddb (n: Nat) : Bool
Oddb n = Notb (Evenb n)

TestOddb1 : Equal Bool (Oddb 1n) Bool.true
TestOddb1 = Equal.refl

TestOddb2 : Equal Bool (Oddb 4n) Bool.false
TestOddb2 = Equal.refl

Naturalmente, nós também podemos definir funções com múltiplos argumentos por recursão.

Plus (n: Nat) (m: Nat) : Nat
Plus  Nat.zero    m = m
Plus (Nat.succ k) m = Nat.succ (Plus k m)

Somar 3n e 2n retornará 5n como esperado. A simplificação que o Kind realiza para chegar a esse valor pode ser visualizada assim:

Plus (Nat.succ (Nat.succ (Nat.succ Nat.zero))) (Nat.succ (Nat.succ Nat.zero))

> Nat.succ (Plus (Nat.succ (Nat.succ Nat.zero)) (Nat.succ (Nat.succ Nat.zero)))
pela segunda regra de Plus

> Nat.succ (Nat.succ (Plus (Nat.succ Nat.zero)) (Nat.succ (Nat.succ Nat.zero)))
pela segunda regra de Plus

> Nat.succ (Nat.succ (Nat.succ (Plus Nat.zero (Nat.succ (Nat.succ Nat.zero)))))
pela segunda regra de Plus

> Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))
pela primeira regra de Plus

A multiplicação pode ser definida usando a definição de Plus, da seguinte forma:

Mult (n: Nat) (m: Nat) : Nat
Mult  Nat.zero    m = Nat.zero
Mult (Nat.succ k) m = Plus m (Mult k m)

TestMult1 : Equal Nat (Mult 3n 3n) 9n
TestMult1 = Equal.refl

Você também pode usar pattern matching em duas expressões ao mesmo tempo:

Minus (n: Nat) (m: Nat) : Nat
Minus  Nat.zero     m           = Nat.zero
Minus  n            Nat.zero    = n
Minus (Nat.succ k) (Nat.succ j) = Minus k j

O função Exp pode ser definida usando Mult (de forma análoga a como se define Mult usando Plus):

Exp (base: Nat) (power: Nat) : Nat
Exp base  Nat.zero    = Nat.succ Nat.zero
Exp base (Nat.succ k) = Mult base (Exp base k)

Factorial

Lembrando da definição matemática básica de fatorial:

\[\mathrm factorial(n) = \begin{cases} \text{se $n$} = 0\,& 1\\ \text{caso contrário}, & n * factorial(n-1) \end{cases} \]

\[ f(x)=\begin{cases}x&(x = 1)\\xf(x-1)&(x\gt 1)\end{cases} , x\in \Bbb{N} \] Traduza a função fatorial para Kind2:

Factorial (n: Nat) : Nat
Factorial n = ?

TestFactorial1 : Equal Nat (Factorial 3n ) 6n
TestFactorial1 = ?

TestFactorial2 : Equal Nat (Factorial 5n) 120n
TestFactorial2 = ?

A função Eql testa a igualdade entre Naturais, retornando um booleano

Eql (n: Nat) (m: Nat) : Bool
Eql  Nat.zero     Nat.zero    = Bool.true
Eql  Nat.zero    (Nat.succ j) = Bool.false
Eql (Nat.succ k)  Nat.zero    = Bool.false
Eql (Nat.succ k) (Nat.succ j) = Eql k j

A função Lte testa se o primeiro argumento é menor ou igual ao segundo, retornando um booleano

Lte (n: Nat) (m: Nat) : Bool
Lte  Nat.zero     m           = Bool.true
Lte (Nat.succ k)  Nat.zero    = Bool.false
Lte (Nat.succ k) (Nat.succ j) = Lte k j

TestLte1 : Equal Bool (Lte 2n 2n) Bool.true
TestLte1 = Equal.refl

TestLte2 : Equal Bool (Lte 2n 4n) Bool.true
TestLte2 = Equal.refl

TestLte3 : Equal Bool (Lte 4n 2n) Bool.false
TestLte3 = Equal.refl

Blt_nat

A função Blt_nat testa a relação "menor que" em números naturais. Em vez de criar uma nova função recursiva, defina ela usando funções previamente definidas.

Blt_nat (n: Nat) (m: Nat) : Bool
Blt_nat n m = ?

Test_blt_nat_1 : Equal Bool (Blt_nat 2n 2n) Bool.false
Test_blt_nat_1 = ?

Test_blt_nat_2 : Equal Bool (Blt_nat 2n 4n) Bool.true
Test_blt_nat_2 = ?

Test_blt_nat_3 : Equal Bool (Blt_nat 4n 2n) Bool.false
Test_blt_nat_3 = ?