OK, this isn't a usual forum post, and most of you are going to laugh at me or get mad or something. But I'm having huge troubles with my homework. I've been to the tutors, TA's , the Professor, and friends. My friends are clueless, and the rest are useless...
So I turn to my fellow organization. I'm in a logical reasoning class, and I'm a little lost on proving theorems. The worst part is, they won't use real english examples in the homework. They use ACL2s programming language that I do understand, but makes the actual problem confusing. If anyone used a non-object-oriented program (scheme etc...) youll understand it. DOES ANYONE HAVE A CLUE ON WHAT TO DO. I'm not looking for answers, just explanations. (but I am open-minded on answers lol
)
PROBLEM 1:
Let’s revisit the finite-set functions we saw in Homework 2.
We take a set to a be a true list of elements. Thus,
(defun setp (l)
(if (endp l)
(equal l nil)
(setp (cdr l))))
Set membership:
(defun set-memberp (a l)
(if (endp l)
nil
(or (equal (car l) a)
(set-memberp a (cdr l)))))
Set inclusion:
(defun set-subsetp (l m)
(if (endp l)
t
(and (set-memberp (car l) m)
(set-subsetp (cdr l) m))))
Set equality:
(defun set-equalp (l m)
(and (set-subsetp l m)
(set-subsetp m l)))
Union and intersection are straightforward:
(defun set-union (l m)
(if (endp l)
m
(cons (car l)
(set-union (cdr l) m))))
(defun set-inter (l m)
(if (endp l)
nil
(if (set-memberp (car l) m)
CSU290 Lecture Notes, Spring 2008 hw4.txt, page 2
(cons (car l) (set-inter (cdr l) m))
(set-inter (cdr l) m))))
Set size - recall that we do not count duplicate elements when we are
considering the size of a set, that is, {a,b,b,c,d} has size 4.
;; remove all occurrences of a from l
(defun remove-element (a l)
(if (endp l)
nil
(if (equal (car l) a)
(remove-element a (cdr l))
(cons (car l) (remove-element a (cdr l))))))
(defun set-size (l)
(if (endp l)
0
(+ 1 (set-size (remove-element (car l) (cdr l))))))
We are asking you to formalize and then prove the following conjectures.
This means that you should go through the following steps for each of
the questions below:
1. Write down a formula that expresses the conjecture we are asking
you to prove.
2. Then, try to prove the formula you came up with. Remember, first
try to come up with counterexample to get a sense of whether what
you are trying to prove is actually true.
3. If you are proving the formula by induction, make sure that you
clearly identify the proof obligations.
Some of these are hard, so make sure that you at least get the formula
you are trying to prove right, and get the proof obligations right.
For (a), recall that recall that a relation R is reflexive if x R x
for all x, a relation R is symmetric if x R y implies y R x for all
x, y, and a relation R is transitive if x R y and y R z implies x R z
for all x,y,z.
For (b)-(e), recall that a binary operation OP is commutative if
(x OP y) = (y OP x) for all x,y, and associative if (x OP (y OP z))
= ((x OP y) OP z) for all x,y,z.
(a) Prove that set-equalp is an equivalence relation, that is, that it
is reflexive, symmetric, and transitive.
(b) Prove that set-union is commutative.
(c) Prove that set-inter is commutative.
(d) Prove that set-union is associative.
(e) Prove that set-inter is associative.
If this thread is allowed moderator. Delete it
So I turn to my fellow organization. I'm in a logical reasoning class, and I'm a little lost on proving theorems. The worst part is, they won't use real english examples in the homework. They use ACL2s programming language that I do understand, but makes the actual problem confusing. If anyone used a non-object-oriented program (scheme etc...) youll understand it. DOES ANYONE HAVE A CLUE ON WHAT TO DO. I'm not looking for answers, just explanations. (but I am open-minded on answers lol
)PROBLEM 1:
Let’s revisit the finite-set functions we saw in Homework 2.
We take a set to a be a true list of elements. Thus,
(defun setp (l)
(if (endp l)
(equal l nil)
(setp (cdr l))))
Set membership:
(defun set-memberp (a l)
(if (endp l)
nil
(or (equal (car l) a)
(set-memberp a (cdr l)))))
Set inclusion:
(defun set-subsetp (l m)
(if (endp l)
t
(and (set-memberp (car l) m)
(set-subsetp (cdr l) m))))
Set equality:
(defun set-equalp (l m)
(and (set-subsetp l m)
(set-subsetp m l)))
Union and intersection are straightforward:
(defun set-union (l m)
(if (endp l)
m
(cons (car l)
(set-union (cdr l) m))))
(defun set-inter (l m)
(if (endp l)
nil
(if (set-memberp (car l) m)
CSU290 Lecture Notes, Spring 2008 hw4.txt, page 2
(cons (car l) (set-inter (cdr l) m))
(set-inter (cdr l) m))))
Set size - recall that we do not count duplicate elements when we are
considering the size of a set, that is, {a,b,b,c,d} has size 4.
;; remove all occurrences of a from l
(defun remove-element (a l)
(if (endp l)
nil
(if (equal (car l) a)
(remove-element a (cdr l))
(cons (car l) (remove-element a (cdr l))))))
(defun set-size (l)
(if (endp l)
0
(+ 1 (set-size (remove-element (car l) (cdr l))))))
We are asking you to formalize and then prove the following conjectures.
This means that you should go through the following steps for each of
the questions below:
1. Write down a formula that expresses the conjecture we are asking
you to prove.
2. Then, try to prove the formula you came up with. Remember, first
try to come up with counterexample to get a sense of whether what
you are trying to prove is actually true.
3. If you are proving the formula by induction, make sure that you
clearly identify the proof obligations.
Some of these are hard, so make sure that you at least get the formula
you are trying to prove right, and get the proof obligations right.
For (a), recall that recall that a relation R is reflexive if x R x
for all x, a relation R is symmetric if x R y implies y R x for all
x, y, and a relation R is transitive if x R y and y R z implies x R z
for all x,y,z.
For (b)-(e), recall that a binary operation OP is commutative if
(x OP y) = (y OP x) for all x,y, and associative if (x OP (y OP z))
= ((x OP y) OP z) for all x,y,z.
(a) Prove that set-equalp is an equivalence relation, that is, that it
is reflexive, symmetric, and transitive.
(b) Prove that set-union is commutative.
(c) Prove that set-inter is commutative.
(d) Prove that set-union is associative.
(e) Prove that set-inter is associative.
If this thread is allowed moderator. Delete it
