6.2. Recursão Estrutural e Terminação
Uma função é definida por recursão estrutural quando cada chamada recursiva é sobre um argumento estruturalmente menor, um construtor mais perto de um caso base. Tal definição termina, e o compilador de equações a transforma em uma aplicação do recursor. O fatorial recorre sobre o predecessor, e Fibonacci tem dois casos base e recorre sobre os dois predecessores.
namespace Func
def fact : ℕ → ℕ
| 0 => 1
| n + 1 => (n + 1) * fact n
def fib : ℕ → ℕ
| 0 => 0
| 1 => 1
| n + 2 => fib n + fib (n + 1)
end Func
Lean admite como definições comuns apenas aquelas que consegue mostrar que terminam, e a razão é a consistência. Uma definição total expõe as suas equações de definição como teoremas utilizáveis e reduz durante a verificação de tipos, então uma equação recursiva como loopy = loopy + 1, se Lean a aceitasse, provaria False por si só. O bloco abaixo postula exatamente essa equação como axioma e deriva a contradição, para mostrar o que uma definição não terminante irrestrita concederia. Lean não gera tal axioma, e rejeita as definições que o produziriam, e é por isso que toda função acima termina. Uma computação que de fato entra em laço ainda pode ser escrita com partial def, mas Lean então mantém a função opaca e não expõe equação alguma, então nenhuma contradição segue.
namespace Func
opaque loopy : ℕ
axiom loopy_eq : loopy = loopy + 1
theorem loopy_false : False := ⊢ False
h:loopy = loopy + 1⊢ False
All goals completed! 🐙
end Func
Para uma recursão que termina por uma razão que Lean não enxerga estruturalmente, termination_by com decreasing_by fornece uma medida e a sua prova, o que o guia trata mais adiante; esta aula fica dentro da recursão estrutural.
6.2.1. Exemplos
Os exemplos abaixo definem funções por recursão estrutural, variam o argumento recursivo e marcam as definições que Lean rejeita.
Example 1. O fatorial e o seu valor em 4.
namespace Func
#eval fact 4
end Func
Example 2. Fibonacci precisa de dois casos base, então o seu caso do passo lê os dois valores precedentes.
namespace Func
example : fib 6 = 8 := rfl
end Func
Example 3. Uma soma dos números de 0 a n, recorrendo sobre o predecessor.
namespace Func
def sumTo : ℕ → ℕ
| 0 => 0
| n + 1 => (n + 1) + sumTo n
example : sumTo 5 = 15 := rfl
end Func
Example 4. A mesma soma com um argumento acumulador, carregando o total corrente para a frente.
namespace Func
def sumAcc : ℕ → ℕ → ℕ
| 0, acc => acc
| n + 1, acc => sumAcc n (acc + (n + 1))
example : sumAcc 5 0 = 15 := rfl
end Func
Example 5. power da Aula 3 é uma recursão aninhada, o seu caso do passo chamando mul sobre o resultado recursivo.
example : power 2 3 = 8 := rfl
Example 6. Uma função pode recorrer sobre o seu primeiro argumento, ao contrário do add da Aula 3 que recorre sobre o segundo.
namespace Func
def countDown : ℕ → List ℕ
| 0 => []
| n + 1 => (n + 1) :: countDown n
example : countDown 3 = [3, 2, 1] := rfl
end Func
Example 7. Duas funções podem recorrer uma através da outra, declaradas juntas com mutual.
namespace Func
mutual
def evn : ℕ → Bool
| 0 => true
| n + 1 => od n
def od : ℕ → Bool
| 0 => false
| n + 1 => evn n
end
example : evn 4 = true := rfl
end Func
Example 8. Uma função total sobre Option, devolvendo um resultado para os dois construtores.
namespace Func
def orZeroList : Option (List ℕ) → List ℕ
| none => []
| some xs => xs
example : orZeroList none = [] := rfl
end Func
Example 9. Uma definição que Lean rejeita. A chamada recursiva é sobre a mesma lista, então nenhum argumento diminui, Lean não consegue ver que ela termina, e não aceita esta equação como uma definição total. O bloco é mostrado, mas não elaborado.
def loopForever {α : Type} : List α → List α
| [] => []
| x :: xs => loopForever (x :: xs)
Example 10. Um caso base em 0 e um passo em n + 1 é a forma de toda recursão sobre ℕ, aqui duplicando por adição repetida.
namespace Func
def twice : ℕ → ℕ
| 0 => 0
| n + 1 => twice n + 2
example : twice 5 = 10 := rfl
end Func