arademaker/cs-fp

Course on Computational Semantics

cs-fp's Issues

comportamento desejado?

CS-FP/FSynF.hs

Line 246 in 1b6e17a

boundVarsInForm :: Formula Term -> [Variable]

λ> boundVarsInForm $ Forall x (Atom "R" [tz,ty])
[x]

c5e24

o primeiro item desse exercício me levou a esta discussão.

outros links: 1 2.

Porque usar o `'` no final do nome?

CS-FP/FSynF.hs

Line 230 in 1b6e17a

termsInForm' :: Formula Term -> [Term]

bound vars

@odanoburu seu exemplo Px \forall x Qx apenas mostra que as funções freeVarsInForm e boundVarsInForm não são complementares como parecem. Na existência de casos como este, não basta retornar uma lista de variáveis, teríamos que diferenciar suas ocorrências. Acho que o mais preciso seria implementarmos outra função antes, que renomeia todas as variáveis garantindo que não exista este tipo de colisão. Algo como as α-conversion em https://en.wikipedia.org/wiki/Lambda_calculus

CS-FP/FSynF.hs

Line 257 in 5f7d327

boundVarsInForm f = intersect (boundVarsInForm' f) (varsInForm f)

definição de Ã

no capítulo 5 do livro (seção 7, p. 108), os autores definem:

The rules of the inference engine are the following. Let à be given by: 
if A is of the form ~C, then à = C, otherwise Ã=~A. 

em que ~A é o complemento de A. pelo que entendi, Ã é equivalente ao complemento de A, de modo que não entendi o propósito dessa definição. entendi errado?