Code Immersion

Here’s the function I tried to show in class; I had put in a couple last minute fixes that actually ended up making it break more often, but now as far as I can tell it corresponds with sentential logic exactly, except that for coding reasons it requires parentheses around negated clauses, which sentential does not. The function is based on the more rigorous definition of sentential, which requires parentheses inserted with every connective (in practice, logicians often leave out the outermost parentheses).


;Determines if the argument is a well-formed formula of sentential logic with basic letters P-S.
;Example calls: (wff? 'P) (wff? '(P v Q)) (wff? '(~ (~ (P & (Q (R v S))))) all return #t
; (wff? 23) (wff? '(P Q v)) (wff? '(P v Q v R)) return #f


(define letters '(P Q R S))
(define connectives '(v & => ))
(define negated '(~P ~Q ~R ~S))


(define wff?
(lambda (formula)
(let ((letter? (lambda (a)
;asks if the argument is a basic letter of sentential
(if (or (member a letters)
(member a negated))
#t
#f))))
(cond
;these conditions check syntactic rules
((letter? formula)
#t)
((list? formula)
(cond
((equal? (cdr formula) '())
#f)
((equal? (cddr formula) '())
#f)
((if (or (and (and (wff? (car formula)) (and (wff? (third formula)) (eq? (cdddr formula) '())))
(member (second formula) connectives))
(and (equal? (car formula) '~) (and (wff? (second formula)) (eq? (cddr formula) '()))))
#t
#f))
(else #f)))
(else #f)))))