code:

(define (uniq lst)
  (if (null? lst) lst
      (let ((ulst (uniq (cdr lst))))
	(if (member (car lst) ulst) ulst lst))))

(uniq '(a b c d e f))
(uniq '((a a) (b b) (c c)))
(uniq '(a a b c a d b c))
(uniq '(a (a a) a (a a) (a a) a))

(define (check-var-i var df)
  (and (member var df) (member (list 'not var) df)))

(define (check-var var df)
  (if (and (list? var) (eqv? 'not (car var)))
      (check-var-i (cadr var) df)
      (check-var-i var df)))

(display "check-var") (newline)

(check-var 'a '(a b c))
(check-var 'a '((not a) b c))
(check-var 'a '((not a) b a c))

(define (simplify-disj df)
  (cond ((null? df) df)
	((equal? '(#f)
		 (uniq (map check-var df
			    (make-list (length df) df))))
	 df)
	(else #t)))

(display "simplify-disj") (newline)

(simplify-disj '(a))
(simplify-disj '(a b c d))
(simplify-disj '((not a) b (not c) d))
(simplify-disj '((not a) b (not c) c d))
(simplify-disj '(a b c a (not c) b a d))
(newline)

(define (filter p l)
  (if (null? l) l
      (if (p (car l))
	  (cons (car l) (filter p (cdr l)))
	  (filter p (cdr l)))))

(lambda (x) (not (eqv? #t x)))

(define (not-#t? x) (not (eqv? #t x)))

(define (simplify-conj cf)
  (if (member #f cf) #f
      (let ((pcnf
	     (uniq (map simplify-disj (filter not-#t? cf)))))
	(if (member #f pcnf) #f
	    (filter not-#t? pcnf)))))

(simplify-conj
 '((a b c d)
   (a (not a) b c d)
   #f
   (a c d)
   (a b c d)))

(simplify-conj
 '((a b c d)
   (a (not a) b c d)
   (a c d)
   (a b c d)))

code:

cat file.scm | guile

code:

;; -*- coding: cyrillic-alternativnyj; -*-
; $Id: knf.scm,v 1.2 2006/05/17 13:39:48 user Exp $

; Нам понадобится работать со списком, как с множеством,
; то есть, надо исключать повторные вхождения.
(define (uniq lst)
  (if (null? lst) lst
      (let ((ulst (uniq (cdr lst))))
	(if (member (car lst) ulst) ulst lst))))

; Проверка:
(uniq '(a b c d e f))
(uniq '((a a) (b b) (c c)))
(uniq '(a a b c a d b c))
(uniq '(a (a a) a (a a) (a a) a))

; Проверяем вхождение переменной и ее отрицания в дизъюнктивную форму.
(define (check-var-i var df)
  (and (member var df) (member (list 'not var) df)))

; Поскольку переменная может встретиться в виде отрицания, 
; возможно, потребуется снять объемлющее "not"
(define (check-var var df)
  (if (and (list? var) (eqv? 'not (car var)))
      (check-var-i (cadr var) df)
      (check-var-i var df)))

; Проверка:
(check-var 'a '(a b c))
(check-var 'a '((not a) b c))
(check-var 'a '((not a) b a c))
(check-var '(not a) '((not a) b a c))

; Упрощение ДФ: исключение повторов, проверка на то,
; что она не сводится к тождественной.
(define (simplify-disj df)
  (cond ((null? df) df)
	((equal? '(#f)
		 (uniq (map check-var df
			    (make-list (length df) df))))
	 df)
	(else #t)))

(begin (display "Testing simplify-disj") (newline))

(simplify-disj '(a))
(simplify-disj '(a b c d))
(simplify-disj '((not a) b (not c) d))
(simplify-disj '((not a) b (not c) c d))
(simplify-disj '(a b c a (not c) b a d))
(newline)

; Выборка членов списка, удовлетворяющих условию p.
(define (filter p l)
  (if (null? l) l
      (if (p (car l))
	  (cons (car l) (filter p (cdr l)))
	  (filter p (cdr l)))))

(define (not-#t? x) (not (eqv? #t x)))

; Упрощение конъюнктивной формы:
; отсечение тождественно ложных и тождественно истинных членов,
; упрощение входящих дизъюнктивных форм, устранение повторов.
(define (simplify-conj cf)
  (if (member #f cf) #f
      (let ((pcnf
	     (uniq (map simplify-disj (filter not-#t? cf)))))
	(if (member #f pcnf) #f
	    (filter not-#t? pcnf)))))

; Проверка
(simplify-conj
 '((a b c d)
   (a (not a) b c d)
   #f
   (a c d)
   (a b c d)))

(simplify-conj
 '((a b c d)
   (a (not a) b c d)
   (a c d)
   (a b c d)))

code:

;; -*- coding: cyrillic-alternativnyj; -*-
; $Id: knf.el,v 1.3 2006/05/17 14:18:22 user Exp $

; Нам понадобится работать со списком, как с множеством,
; то есть, надо исключать повторные вхождения.
(defun uniq (lst)
  (if (null lst) lst
      (let ((ulst (uniq (cdr lst))))
	(if (member (car lst) ulst) ulst lst))))

; Проверка:
(uniq '(a b c d e f))
(uniq '((a a) (b b) (c c)))
(uniq '(a a b c a d b c))
(uniq '(a (a a) a (a a) (a a) a))

; Проверяем вхождение переменной и ее отрицания в дизъюнктивную форму.
(defun check-var-i (var df)
  (and (member var df) (member (list 'not var) df)))

; Поскольку переменная может встретиться в виде отрицания, 
; возможно, потребуется снять объемлющее "not"
(defun check-var (var df)
  (if (and (listp var) (eq 'not (car var)))
      (check-var-i (cadr var) df)
      (check-var-i var df)))

; Проверка:
(check-var 'a '(a b c))
(check-var 'a '((not a) b c))
(check-var 'a '((not a) b a c))
(check-var '(not a) '((not a) b a c))

(defun maplist (f l)
  (if (null l) l
    (cons (apply f (list (car l))) (maplist f (cdr l)))))
(defun mapl (f l)
  (if (member nil l) nil
    (cons (apply f (maplist 'car l))
	  (mapl f (maplist 'cdr l)))))
(defun map (f &all l) (mapl f l))

; Упрощение ДФ: исключение повторов, проверка на то,
; что она не сводится к тождественной.
(defun simplify-disj (df)
  (cond ((null df) df)
	((equal '(nil)
		 (uniq (mapl 'check-var (list df
			    (make-list (length df) df)))))
	 df)
	(t t)))

(simplify-disj '(a))
(simplify-disj '(a b c d))
(simplify-disj '((not a) b (not c) d))
(simplify-disj '((not a) b (not c) c d))
(simplify-disj '(a b c a (not c) b a d))
(newline)




; Выборка членов списка, удовлетворяющих условию p.
(defun filter (p l)
  (if (null l) l
      (if (apply p (list (car l)))
	  (cons (car l) (filter p (cdr l)))
	  (filter p (cdr l)))))

(defun not-t (x) (not (eq t x)))

; Упрощение конъюнктивной формы:
; отсечение тождественно ложных и тождественно истинных членов,
; упрощение входящих дизъюнктивных форм, устранение повторов.
(defun simplify-conj (cf)
  (if (member nil cf) nil
      (let ((pcnf
	     (uniq (mapl 'simplify-disj (list (filter 'not-t cf))))))
	(if (member nil pcnf) nil
	    (filter 'not-t pcnf)))))


; Проверка
(simplify-conj
 '((a b c d)
   (a (not a) b c d)
   nil
   (a c d)
   (a b c d)))

(simplify-conj
 '((a b c d)
   (a (not a) b c d)
   (a c d)
   (a b c d)))

code:

===================================================================
RCS file: RCS/knf.scm,v
retrieving revision 1.2
diff -u -r1.2 knf.scm
--- knf.scm	2006/05/17 13:39:48	1.2
+++ knf.scm	2006/05/17 17:48:09
@@ -1,5 +1,5 @@
 ;; -*- coding: cyrillic-alternativnyj; -*-
-; $Id: knf.scm,v 1.2 2006/05/17 13:39:48 user Exp $
+; $Id: knf.scm,v 1.4 2006/05/17 17:46:17 user Exp $
 
 ; Нам понадобится работать со списком, как с множеством,
 ; то есть, надо исключать повторные вхождения.
@@ -31,15 +31,17 @@
 (check-var 'a '((not a) b a c))
 (check-var '(not a) '((not a) b a c))
 
+; Проверка на то, что все члены списка равны заданному.
+(define (all? el lst) (equal? (list el) (uniq lst)))
+
 ; Упрощение ДФ: исключение повторов, проверка на то,
 ; что она не сводится к тождественной.
 (define (simplify-disj df)
-  (cond ((null? df) df)
-	((equal? '(#f)
-		 (uniq (map check-var df
-			    (make-list (length df) df))))
-	 df)
-	(else #t)))
+  (cond
+   ((all? #f df) #f)
+;    ((member #t df) #t)
+   ((all? #f (map check-var df (make-list (length df) df))) df)
+   (else #t)))
 
 (begin (display "Testing simplify-disj") (newline))
 
@@ -48,14 +50,14 @@
 (simplify-disj '((not a) b (not c) d))
 (simplify-disj '((not a) b (not c) c d))
 (simplify-disj '(a b c a (not c) b a d))
+(simplify-disj '(#f #f #f))
 (newline)
 
 ; Выборка членов списка, удовлетворяющих условию p.
 (define (filter p l)
-  (if (null? l) l
-      (if (p (car l))
-	  (cons (car l) (filter p (cdr l)))
-	  (filter p (cdr l)))))
+  (cond ((null? l) l)
+	((p (car l)) (cons (car l) (filter p (cdr l))))
+	(else (filter p (cdr l)))))
 
 (define (not-#t? x) (not (eqv? #t x)))
 
@@ -82,3 +84,11 @@
    (a (not a) b c d)
    (a c d)
    (a b c d)))
+
+(simplify-conj
+ '((a b c d)
+   (a (not a) b c d)
+   (a c d)
+   (#f #f)
+   (a c d c)
+   (a b c d)))

Quote:

---

Ну теперь-то я знаю, как выглядит удобный, читабельный и интуитивно-очевидный код, которого так не хватает всем этим ламерским ООП-языкам

---