Laws of Form

[Kragen Sitaker]

A few simple Scheme programs to create and evaluate Laws of Form
expressions.

By the way, in the original text, (expr) was represented as something like

____
    |
expr|

; evaluate Laws of Form expressions.
; Kragen Sitaker, 1999-03-16, for fun
; A cross is a list.
; The whole expression is a list too, which is confusing.
; so the empty expression is (  );
; the expression of one cross is ( () );
; the expression of two adjacent crosses is ( ()() );
; the expression of one cross inside another is ( (()) ).
;
; There are two basic reductions: ( (()) ) -> (  ), and ( ()() ) -> ( () ).
;
; With those two basic reductions, you can reduce any expression to either
; (  ) or ( () ).
;
; So ( ((())) ) becomes ( () ) by the first reduction. ( ((()))() ) becomes
; ( ()() ) by the first reduction, then ( () ) by the second reduction.
;
; I will do the simple thing and express the values internally as #t or #f.
; #t will represent ( () ), and #f will represent (  ).

; If none of this makes any sense to you, it may be because you
; haven't read the book (_Laws of Form_).  Briefly, it's about a very
; simple formalism for Boolean logic, written by a brilliant guy who
; (later?) became a nutcase.

; Essentially, a "cross" is like a NAND or a NOR (depending on which
; interpretation you choose; by the interpretation I'm using internally,
; it's a NOR.)  Laws of Form expressions are very easy to evaluate by
; hand; since the representation for one of the two values is the null
; string, then a subexpression that evaluates to that value simply 
; disappears from the expression.  No need for the 1 AND X -> X 
; transformation; it happens automatically as a consequence of the notation.

(define (lof-eval-helper expr)
  (cond ((null? expr)          #f)
	((lof-eval (cdr expr)) #t)
	(#t                    (not (lof-eval (car expr))))
  )
)

(define (lof-eval expr)
  (if (lof-eval-helper expr) '(()) '())
)

; This transforms an ordinary Boolean expression into LOF-notation.
; Again, #f becomes the empty string, and #t becomes a single cross.
; Grammar:
; expr -> #f | #t | (and expr expr) | (or expr expr) | (not expr) | symbol
; This really feels quite crude, and it's sort of voodooish.  It uses the
; opposite internal representation of true and false that lof-eval-helper
; does.  (I realized this after I finished writing it, which is why I think
; it's kind of voodooish.)  It ends up working the same way because everything
; gets wrapped in one fewer set of parentheses.

(define (lof-transform expr)

  (define (lof-and args)
    (if (null? (cddr args))
	(cons (cons (lof-transform (car args))
		    (cons (lof-transform (cadr args)) '())
	      )
	)
	(error 'and-got-wrong-number-of-args (cons 'and args))
    )
  )

  (define (lof-or args)
    (if (null? (cddr args))
	(cons (cons (lof-transform (car args)) '())
	      (cons (cons (lof-transform (cadr args)) '()) '())
        )
	(error 'or-got-wrong-number-of-args (cons 'or args))
    )
  )

  (define (lof-not args)
    (if (null? (cdr args))
	(cons (lof-transform (car args)) '())
	(error 'not-got-wrong-number-of-args (cons 'not args))
    )
  )

  (cond ((eq? expr '#f) '())
	((eq? expr '#t) '(()))
	((pair? expr)
	 (let ((head (car expr)))
	   (cond ((eq? head 'and) (lof-and (cdr expr)))
		 ((eq? head 'or)  (lof-or (cdr expr)))
		 ((eq? head 'not) (lof-not (cdr expr)))
		 (#t (error 'unimplemented-operator head))
	   )
         )
	)
	((symbol? expr) expr)
	(#t (error 'invalid-boolean-expression expr))
  )
)

; In general, (lof-eval-helper (lof-transform expr)) should give you the
; boolean evaluation of 'expr'.  (As long as it doesn't contain any
; symbols.)

; lof-transform can produce expressions with symbols in them.
; Here is a symbol-substitution thingy to go through and substitute
; expressions for the symbols.

(define (lof-substitute expr alist)
  (cond ((null? expr) '())
	((pair? expr) (cons (lof-substitute (car expr) alist) 
			 (lof-substitute (cdr expr) alist)
		   )
	)
	((symbol? expr)
	 (let ((replpair (assq expr alist)))
	   (if replpair (cdr replpair) expr)
	 )
	)
	(#t (error 'invalid-boolean-expression expr))
  )
)

; OK, so now that we have expressions with variables, we can talk about
; simplifying them.  (Expressions without variables, of course, just simplify
; to 'true' or 'false'.)
; There are several basic simplifications:
; ((expr)) -> expr
; (() expr) -> (())
; ((()) expr) -> (expr)
; (a b) -> (b a)
; 
; And, of course, subexpressions without variables in them can be simplified by
; means of lof-eval.
;
; I'm not sure how to implement these, though.  And they're not sufficient, anyway.
; Try (lof-transform '(or a (not a))) -- the result should simplify to (()), but
; I don't see an obvious way to do it.  And (lof-transform '(or (and a b) 
; (and (not a) b))) should simplify to b.  I don't see any kind of simple way to
; do this.
;
; This is sort of silly, since the whole rationale for doing this was to see how
; to simplify Boolean expressions expressed as LOF expressions.
;
; Of course, determining whether a particular Boolean expression simplifies to
; #f is the SAT problem, so I shouldn't expect a simple, easy solution here.