3.5. Avaliação
O comando #eval executa um programa pelo compilador de Lean, e #reduce normaliza um termo simbolicamente no kernel. Ambos computam 9 abaixo, e #eval é o comando a usar em escala.
#eval add 2 7
#reduce add 2 7
A avaliação dá significado às expressões aritméticas de AExp. Um ambiente leva nomes de variáveis a valores inteiros, e eval reduz uma expressão ao seu valor.
def eval (env : String → ℤ) : AExp → ℤ
| AExp.num i => i
| AExp.var x => env x
| AExp.add e₁ e₂ => eval env e₁ + eval env e₂
| AExp.sub e₁ e₂ => eval env e₁ - eval env e₂
| AExp.mul e₁ e₂ => eval env e₁ * eval env e₂
| AExp.div e₁ e₂ => eval env e₁ / eval env e₂
A divisão por zero não falha. A divisão inteira de Lean é total, com x / 0 = 0, e a avaliação abaixo computa de acordo. O comando #eval e a nossa função eval não têm relação, apesar dos nomes.
#eval eval (fun _ => 7)
(AExp.div (AExp.var "y") (AExp.num 0))
A computação também é um método de prova. Uma equação cujos dois lados avaliam para o mesmo valor vale por rfl, o termo que a Aula 2 usou para n * n = 9 na testemunha 3. Esta é a computação definicional, e ela resolve qualquer equação fechada, isto é, sem variáveis.
example : add 2 7 = 9 := rfl
example : eval (fun _ => 7)
(AExp.div (AExp.var "y") (AExp.num 0)) = 0 := rfl
3.5.1. Exemplos
Os exemplos abaixo executam as funções desta aula e examinam a aritmética que eval herda de ℤ.
Exemplo 1. O décimo número de Fibonacci, computado pelo compilador.
#eval fib 10
Exemplo 2. O fatorial de cinco, pela recursão de mul e add.
#eval factorial 5
Exemplo 3. Dois elevado a dez, pela recursão de power.
#eval power 2 10
Exemplo 4. #reduce normaliza no kernel e chega ao mesmo valor.
#reduce half 7
Exemplo 5. Uma função em Bool avalia para um valor booleano.
#eval evenb 10
Exemplo 6. A avaliação executa funções polimórficas também.
#eval reverse [1, 2, 3]
Exemplo 7. O ambiente fornece o valor de cada variável, e o resto é aritmética.
#eval eval (fun x => if x = "x" then 3 else 0)
(AExp.add (AExp.var "x") (AExp.num 4))
Exemplo 8. A divisão inteira trunca, então 5 / 2 avalia para 2.
#eval eval (fun _ => 0)
(AExp.div (AExp.num 5) (AExp.num 2))
Exemplo 9. A divisão sobre ℤ segue a convenção euclidiana, cujo resto nunca é negativo, então −7 / 2 avalia para −4, e não para −3.
#eval eval (fun _ => 0)
(AExp.div (AExp.num (-7)) (AExp.num 2))
Exemplo 10. Cada avaliação acima serve também como prova, já que rfl fecha uma equação cujos lados computam para o mesmo valor.
example : sumTo 10 = 55 := rfl
example : twoPow 8 = 256 := rfl