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:
(define (ev xs)
(eval `(with-vars ,(free-vars xs) ,xs)))
(define-syntax-rule (tauta fm) (ev 'fm))
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.
#lang racket
;; (with-vars (P Q ) (or Q (or (not P) P))) builds:
;; (for/and [(P (in-list (list #t #f)))] (for/and [(Q (in-list (list #t
#f)))] (or Q (or (not P) P))))
(define-syntax with-vars
(syntax-rules ()
((with-vars (v) cm) (for/and [(v (in-list (list #t #f)))] cm))
((with-vars (w v ...) cm)
(for/and [(w (in-list (list #t #f)))] (with-vars (v ...) cm))) ))
;; flattens a list; for instance, (or (not P) Q) becomes (or not P Q)
(define (flatten lst)
(cond ((null? lst) '())
((pair? (car lst)) (append (flatten (car lst)) (flatten (cdr lst))))
(else
(cons (car lst) (flatten (cdr lst))))))
;; gets the variables in a wff. For instance (free-vars ' (or Q (or (not P)
P)))
;; produces (P Q)
(define (free-vars s)
(let loop [(x (flatten s))]
(cond [(null? x) x]
[(member (car x) '(and or then -> <-> not
equiv display displayln)) (loop (cdr x))]
[(member (car x) (cdr x)) (loop (cdr x))]
[else (cons (car x) (loop (cdr x)))] )))
(define (then x y) (or y (not x)))
(define (equiv x y) (and (then x y) (then y x)))
;; I want to avoid this step. (ev '(or Q (or (not P) P)))) gets the list
;; (P Q) of free variables, builds and evals (with-vars (P Q) (or Q (or
(not P) P))).
(define (ev xs)
(eval `(with-vars ,(free-vars xs) ,xs)))
(define-syntax-rule (tauta fm) (ev 'fm))
; (tauta (or (then P Q) (then Q (not P))))
; (tauta (or P (not P))) ; excluded middle
; (tauta (or (and P Q) (or (not P) (not Q))))
; (tauta (equiv (then P Q) (then (not Q) (not P)))) ;equiv
; (tauta (then (and (then (not A) B) (then (not A) (not B))) A)) ;reductio
ad absurdum
; (tauta (equiv (not (and A B)) (or (not A) (not B)))) ; De Morgan's law
____________________
Racket Users list:
http://lists.racket-lang.org/users
