<div dir="ltr"><div>In general, I don't have problems with macros in Common Lisp or in Scheme. However, macros in Racket baffle me. I simply cannot figure out how syntax->datum, syntax->list and datum->syntax work. In any case, I need a macro to prove that a proposition is a tautology. Below you will find what I did. There are a few examples on how to run the program. What bothers me in this program is the need of calling ev on a quoted version of the fm wff:<br>
<br>(define (ev xs)<br>  (eval `(with-vars ,(free-vars xs) ,xs)))<br><br>(define-syntax-rule (tauta fm) (ev 'fm))<br><br></div>I suppose that one can avoid calling eval by a judicious use of syntax->datum, syntax->list and datum->syntax. I would appreciate suggestions to improve the program.<br>
<div><br><br><br>#lang racket<br><br></div><div>;; (with-vars (P Q ) (or Q (or (not P) P))) builds:<br>;;   (for/and [(P (in-list (list #t #f)))] (for/and [(Q (in-list (list #t #f)))] (or Q (or (not P) P))))<br></div><div>
(define-syntax with-vars<br>  (syntax-rules ()<br>    ((with-vars (v) cm) (for/and [(v (in-list (list #t #f)))] cm)) <br>    ((with-vars (w v ...) cm) <br>     (for/and [(w (in-list (list #t #f)))] (with-vars (v ...) cm))) ))<br>
<br></div><div>;; flattens a list; for instance, (or (not P) Q) becomes (or not P Q)<br></div><div>(define (flatten lst)<br>  (cond ((null? lst) '())<br>        ((pair? (car lst)) (append (flatten (car lst)) (flatten (cdr lst))))<br>
        (else<br>          (cons (car lst) (flatten (cdr lst))))))<br><br></div><div>;; gets the variables in a wff. For instance (free-vars ' (or Q (or (not P) P))) <br></div><div>;; produces (P Q)<br></div><div>(define (free-vars s)<br>
  (let loop [(x (flatten s))]<br>    (cond [(null? x) x]<br>          [(member (car x) '(and or then -> <-> not<br>                                 equiv display displayln)) (loop (cdr x))]<br>          [(member (car x) (cdr x)) (loop (cdr x))]<br>
          [else (cons (car x) (loop (cdr x)))] )))<br><br>(define (then x y) (or y (not x)))<br><br>(define (equiv x y) (and (then x y) (then y x)))<br><br></div><div>;; I want to avoid this step. (ev  '(or Q (or (not P) P)))) gets the list<br>
</div><div>;; (P Q) of free variables, builds and evals (with-vars (P Q) (or Q (or (not P) P))).</div><div>(define (ev xs)<br>  (eval `(with-vars ,(free-vars xs) ,xs)))<br><br>(define-syntax-rule (tauta fm) (ev 'fm))<br>
<br>; (tauta (or (then P Q) (then Q (not P))))<br>; (tauta (or P (not P))) ; excluded middle<br>; (tauta (or (and P Q) (or (not P) (not Q))))<br>;  (tauta (equiv (then P Q) (then (not Q) (not P)))) ;equiv<br>; (tauta (then (and (then (not A) B) (then (not A) (not B))) A)) ;reductio ad absurdum<br>
; (tauta (equiv (not (and A B)) (or (not A) (not B)))) ; De Morgan's law<br><br>
</div></div>