; My naive attempt to generate random propositional formula
; recursively, giving equal probability to standard logical
; constants true and nil and connectives not, and, and ->
; failed:
(set 'random-formula
(lambda()
(amb true
nil
(list 'not (random-formula))
(list 'and (random-formula) (random-formula))
(list 'or (random-formula) (random-formula))
(list '-> (random-formula) (random-formula)))))
(dotimes(i 30)(println i ". " (random-formula)))
; The problem is in infinite recursion. The expectation is that
; random-formula will call seven times another instance of random-formula
; in 6 calls, so it is unlikely that random formula construction
; will be completed. This time, solution is very simple:
(seed (date-value))
(set 'random-formula
(lambda()
(amb true true
nil nil
(list 'not (random-formula))
(list 'and (random-formula) (random-formula))
(list 'or (random-formula) (random-formula))
(list '-> (random-formula) (random-formula)))))
(dotimes(i 20)(println i ". " (random-formula)))
; The results:
0. (not (and (not (and true nil)) (-> (-> (or (and nil nil) nil) true) nil)))
1. true
2. true
3. nil
4. nil
5. (not (not (-> (not nil) true)))
6. (and true (-> true (or (or (or (and true nil) nil) nil) (not (or (not (-> true
(not (or (not (not (or true (and (not true) true)))) (-> nil nil))))) (-> nil
(-> (and nil true) (and (-> (or (or (not (-> true true)) (and (-> nil nil) nil))
(or nil (not true))) (or nil (or true (or true (not nil))))) true))))))))
7. nil
8. nil
9. (or (and nil (not true)) true)
10. (or true (and true (or (or (or nil (not true)) (-> (-> nil (and (or nil true
) nil)) true)) (and (-> nil (or nil nil)) true))))
11. true
12. true
13. (not nil)
14. nil
15. true
16. (and nil (and (-> (or true (or true (-> true (not (-> (or (and (and nil nil)
(not nil))(not nil)) nil)))))(and (and true (or true (-> nil (or true nil))))
(not (and nil nil)))) (or true (and (-> nil (and true (or (not (not (and
(or true nil) (or (and nil (not (or (not (and nil (not true))) true)))(not (not
nil)))))) nil))) true))))
17. (or nil (-> (and nil true) true))
18. nil
19. (and (not (not nil)) (or (or nil (and (not (-> (or (-> nil nil) true) (not (
not (and (or (or (and (not nil) (and true true)) true) true) true))))) (not true)))
nil))
; Now, it is possible, but unlikely that random-formula will
; generate random-formula calls infinitely. In eight function calls,
; new function call will be generated seven times.
;
; Interesting question that occurs immidietely is: but, how big
; is average formula generated on this way? By size of the formula,
; we'll simply count number of connectives and constants in formula,
; i.e. number of nodes in imagined graph. Size of (or true (not nil))
; is, for example, four.
; We'll estimate of average length of formula using the fact that
; Random formula is defined recursively. Let us denote *expected length*
; of average formula as x. Then
;; 1 + 1 + 1 + 1 + (1+x) + (1+2x) + (1+2x) + (1+2x)
; x = --------------------------------------------------
; 8
;
; where 1, 1, 1, 1 are sizes of the trivial formulas: true, true,
; nil and nil; (1+x) is expected size of the formula (list 'not (random-formula))
; and (1+2x) is expected size of other three formulas.
;
; If we solve that equation, we'll get x=8. Let us test that:
(set 'size-of
(lambda(f)
(cond ((or (= f true) (= f nil)) 1)
((= (first f) 'not) (+ (size-of (last f)) 1))
(true (+ (size-of (nth 1 f))
(size-of (nth 2 f))
1)))))
(set 'sum 0)
(dotimes(i 100000)
(inc sum (size-of (random-formula))))
(println (div sum 100000)) ; 8.01414 - OK
; Now, when we are here, we'll try to answer the next question:
; How to define the function that generates random formulas of
; expected length, say, 20. For that purpose, we need slightly
; redefined, more general, random-formula. Instead of repeating
; true and nil two times, we'll repeat it a times, where a is
; real number.
(set 'random-formula
(lambda(a)
(let ((r (random 0 (add 4 (mul 2 a)))))
(cond
((<= 0 r 1) (list 'not (random-formula a)))
((<= 1 r 2) (list 'and (random-formula a) (random-formula a)))
((<= 2 r 3) (list 'or (random-formula a) (random-formula a)))
((<= 3 r 4) (list '-> (random-formula a) (random-formula a)))
((<= 4 r (add 4 a)) true) ; if a=2 then
((<= (add 4 a) r (add 4 a a)) nil)))))
(set 'sum 0)
(dotimes(i 100000)
(inc sum (size-of (random-formula 2))))
(println (div sum 100000)) ; 7.93368 - OK
; Now, my formula for estimation of expected size will get
; this form:
;; (1+x) + (1+2x) + (1+2x) + (1+2x) + 2a
; x = ----------------------------------------
; 6+2a
;
; If we express a explicitly,
;
; 3x + 4
; a = ------
; 2(x-1)
;
; particularly, for x=20, a=1.684210.
(set 'sum 0)
(dotimes(i 100000)
(inc sum (size-of (random-formula 1.6842105))))
(println (div sum 100000)) ; 19.74605 - not bad either.
; Finally, for convenience, we'll redefine random-formula so it
; accepts x as variable, not a.
(set 'random-formula
(lambda(x)
(letn ((a (div (add (mul x 3) 4) (mul 2 (sub x 1))))
(r (random 0 (add 4 (mul 2 a)))))
(cond
((<= 0 r 1) (list 'not (random-formula x)))
((<= 1 r 2) (list 'and (random-formula x) (random-formula x)))
((<= 2 r 3) (list 'or (random-formula x) (random-formula x)))
((<= 3 r 4) (list '-> (random-formula x) (random-formula x)))
((<= 4 r (add 4 a)) true) ; if a=2 then
((<= (add 4 a) r (add 4 a a)) nil)))))
(set 'sum 0)
(dotimes(i 100000)
(inc sum (size-of (random-formula 100))))
(println (div sum 100000)) ; 98.71964
(exit)
---
