Com a aproximação do SupGen, vou postar alguns conteúdos técnicos que provavelmente não darão certo porque não são sobre inteligência artificial pura, mas mesmo assim quero fazer. Aqui estão algumas reflexões sobre totalidade e término. Em Agda (e Lean?), a terminação é garantida por "recursão estrutural", o que significa que os argumentos podem diminuir em "ordem lexicográfica". Entende o que isso significa? Pois é, eu também não. Mas, na verdade, é bem simples. Suponha que você tenha uma cláusula como: foo : Nat → Nat foo (S a) (S b) (S c) (S d) = foo (S a) (S b) c (S (S (S d))) foo x = x Está sendo encerrado? Não está? Como saber? Em Agda, funciona assim: Etapa 0: - argumento 0 no lado esquerdo: (S a) - argumento 0 no lado direito: (S a) — Isto é *idêntico*, então, verifique o próximo argumento. (nota: LHS/RHS significa lado esquerdo/direito da equação) Passo 1: - argumento 1 no lado esquerdo: (S b) - argumento 1 no lado direito: (S b) — Isto é *idêntico*, então, verifique o próximo argumento. Etapa 2: - argumento 2 no lado esquerdo: (S c) - argumento 2 no lado direito: c - Isto é *menor*, portanto, esta cláusula está terminando! E terminamos. Resumindo, sempre que houver uma chamada recursiva no lado direito, basta comparar seus argumentos com os padrões correspondentes no lado esquerdo, um por um, até que um seja menor. Simples, não é? (Quem me dera tivessem explicado assim...) Agora, considere o seguinte: foo : Par -> Par foo (Par (S a) (S b)) = foo (P a (S (S (S b)))) foo x = x Esta função está sendo finalizada? Bem, de acordo com o Agda... não! No entanto, é evidente que sim, pela mesma lógica: como o primeiro componente é menor, o fato do segundo ser maior é irrelevante. Parece que o verificador do Agda está programado para dividir os argumentos em partes menores. Portanto, essa cláusula, como está escrita, não passará pelo verificador, mesmo que termine. Por que estou falando sobre isso? Estava revisando o gerador de recursão do SupGen e percebi que ele poderia ficar mais limpo *e* mais rápido com algumas alterações. Mas será que essas alterações são válidas? Testei e, para minha surpresa, o SupGen estava gerando programas que não terminavam... de acordo com o Agda. A princípio, presumi que minha abordagem estava errada, mas, na verdade, o Agda que estava errado. Agora você tem um novo conhecimento. Tenho certeza de que isso lhe será útil eventualmente!
O novo algoritmo usado pelo SupGen para gerar chamadas recursivas que terminam é muito mais simples *e* mais geral!
