função para medir tamanho de fórmula

[arademaker]

Seguindo as idéia de http://link.springer.com/article/10.1007/BF01531029. podemos implementar uma função que calcula o length de uma formula:

"By the length of a formula we mean the number of binary connectives in the formula..."

[paulodt]

Enviei um pull request, juntamente com o Rafael @rkatz36368.

[arademaker]

versão inicial ainda não testada em 5d6a10c

[paulodt]

versão com recursão de cauda em 6903ec2

[arademaker]

@paulodt tente explicar sua idéia neste issue antes de reimplementar. Descreva como vc espera que sua função trabalhe com uma dada entrada, o passo-a-passo.

[paulodt]

Passo a passo: a função avalia o primeiro elemento da fórmula. Caso ele seja atômico, ela testa se ele está contido na lista dos conectivos binários (and or implies equiv). Se estiver, incrementa o contador (n) em 1 unidade e continua a recursão em cauda. Caso não, ele continua a recursão sem incrementar. Porém, se o elemento não for atômico, há o problema: em quanto eu devo incrementar o contador em quantas unidades? Para isso, a forma mais simples que encontrei foi aplicar a recursão, em cauda, sobre essa lista. O valor que a recursão retornar eu adiciono ao contador e continuo minha recursão principal.

[arademaker]

Fechar quando tivermos alguns testes, vide #37

[paulodt]

Testes com casos que antes causavam ou causariam problema e agora estão solucionados:
"KRR-USER[11]> (test length-form
(is (= 0 (length-form 'A)))
(is (= 0 (length-form 'implies)))
(is (= 1 (length-form '(implies A B))))
(is (= 16940 (length-form (all-clauses)))))

LENGTH-FORM

KRR-USER[12]> (run! 'length-form)

Running test LENGTH-FORM ....
Did 4 checks.
Pass: 4 (100%)
Skip: 0 ( 0%)
Fail: 0 ( 0%)

NIL"
Função criada por mim. Correções finais feitas por @hcrespo.
Creio que mediante tais testes o issue pode ser fechado.

[arademaker]

O (is (= 0 (length-form 'implies))) nem deveria funcionar, não é uma WFF, né? Mas enfim. vou fechar o issue.