; Problem 3 is a tree problem where we need to implement the following
; operations:
; size: such that (size T N) is true if tree T has size N. Note the
; following: (size emptyTree 0) is true.
; (size (tree Leaf) 1) is true.
; (size ((lefttree) root (righttree)) N) is equal to
; (+ 1 (+ (size lefttree X) (size righttree Y)))
; depth: should return the depth of the tree. Note the following:
; (depth emptyTree 0) is true.
; (depth (tree Leaf) 1) is true.
; (depth ((lefttree) root (righttree)) N) is equal to
; (+ 1 (the greater of (depth lefttree) and (depth righttree)))
; remove: such that (remove T1 T2 T3) is true if T3 is formed from T1 by
; removing subtree T2. Note the following:
; (remove T1 emptyTree T1) is true.
; (remove T1 T1 emptyTree) is true.
; (remove (L M R) L (emptyTree M R)) is true.
; (remove (L M R) R (L M emptyTree)) is true.
; (remove (L M R) X Y) from (remove L X (lefttree Y))
; (remove (L M R) X Y) from (remove R X (righttree Y))
; Hmm. Interesting set of problems. Well, size can be built from the
; following sets of base inferences:
(infer (size (tree Leaf) 1))
(infer (size (tree emptyTree) 0))
(infer (size (tree L M R) (+ 1 (+ X Y))) from (size L X) (size R Y))
; This should encode size, but as shaky as I am with Prolog, I will make no
; guarantees.
; Now, depth is a little more complicated. Its basic inferences are as
; follows:
(infer (depth (tree Leaf) 1))
(infer (depth (tree emptyTree) 0))
(infer (depth (tree L M R) (+ 1 X)) from (depth L X) (depth R Y) (> X Y))
(infer (depth (tree L M R) (+ 1 Y)) from (depth L X) (depth R Y) (> Y X))
; If this works, it should code depth. But again, I'm not guaranteeing it.
; Now, the most complex inference for this problem is remove. Its basic
; inferences are:
(infer (remove X (tree emptyTree) X))
(infer (remove X X (tree emptyTree)))
(infer (remove (tree L M R) X (tree A B C)) from (remove L X A))
(infer (remove (tree L M R) X (tree A B C)) from (remove R X C))