Just For Fun: Model-Theoretic Semantics of First-Order Logic Expressed in Racket

Show & Tell
1

This is a faithful implementation of the (uninteresting) model-theoretic (Tarskian) semantics of first-order logic in Racket. We assume that domains are finite. This program is written for people to read, and only incidentally for machines to execute.

Syntax:

<term> ::= <var> | (<func> <term>*)
<predicate> ::= (<pred> <term>*)
<exp> ::= <bool>
       |  <predicate>
       |  (not <exp>)
       |  (and <exp> <exp>)
       |  (or <exp> <exp>)
       |  (=> <exp> <exp>)
       |  (<=> <exp> <exp>)
       |  (forall <var> <exp>)
       |  (exists <var> <exp>)

Preliminaries:

(define (forall? pred lst)
  (cond ((null? lst) #t)
        ((pred (car lst))
         (forall? pred (cdr lst)))
        (else #f)))
(define (exists? pred lst)
  (cond ((null? lst) #f)
        ((pred (car lst)) #t)
        (else
         (exists? pred (cdr lst)))))
(struct interp (domain func pred))
(define (funcval m f)
  ((interp-func m) f))
(define (predval m p)
  ((interp-pred m) p))
(define ((termval m v) term)
  (match term
    (,x (guard (symbol? x)) (v x))
    ((,func . ,term*)
     (apply (funcval m func)
            (map (termval m v) term*)))))
(define undefined
  (lambda (x)
    (error 'undefined "unknown variable ~s" x)))
(define (extend v x a)
  (lambda (y)
    (if (eq? y x)
        a
        (v y))))

Semantics:

(define (holds? m v exp)
  (match exp
    (,b (guard (boolean? b)) b)
    ((not ,e) (not (holds? m v e)))
    ((and ,e1 ,e2) (and (holds? m v e1)
                        (holds? m v e2)))
    ((or ,e1 ,e2) (or (holds? m v e1)
                      (holds? m v e2)))
    ((=> ,e1 ,e2) (or (not (holds? m v e1))
                      (holds? m v e2)))
    ((<=> ,e1 ,e2) (eq? (holds? m v e1)
                        (holds? m v e2)))
    ((forall ,x ,e)
     (forall? (lambda (a)
                (holds? m (extend v x a) e))
              (interp-domain m)))
    ((exists ,x ,e)
     (exists? (lambda (a)
                (holds? m (extend v x a) e))
              (interp-domain m)))
    ((,pred . ,term*)
     (apply (predval m pred)
            (map (termval m v) term*)))))

Note that I do not use the match of Racket.

An Example (Modular Arithmetic):

(define (mod-interp n)
  (interp (range n)
          (lambda (f)
            (case f
              ((zero) (lambda () 0))
              ((one) (lambda () (modulo 1 n)))
              ((+) (lambda (a b)
                     (modulo (+ a b) n)))
              ((*) (lambda (a b)
                     (modulo (* a b) n)))
              (else (error 'mod-interp "unknown func symbol ~s" f))))
          (lambda (p)
            (case p
              ((=) (lambda (a b) (= a b)))
              (else (error 'mod-interp "unknown pred symbol ~s" p))))))

> (define modulo_inverse_existence
    '(forall x (=> (not (= x (zero)))
                   (exists y (= (* x y) (one))))))
> (filter (lambda (n)
            (holds? (mod-interp n) undefined
                    modulo_inverse_existence))
          (range 1 100))
'(1 2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 59 61 67 71 73 79 83 89 97)
3 Likes
2

@ulambda, this is really cool.

When you say "uninteresting", what do you mean by that?

1 Like
3

I say it in the sense of Jean-Yves Girard, a proof theorist. I refer you to his books "Proofs and Types" and "The Blind Spot".

2 Likes