1#| 2(defpkg "M1" 3 '(defun declare ignore xargs defthm mutual-recursion 4 include-book in-theory disable defconst 5 defmacro &rest 6 intern-in-package-of-symbol 7 coerce symbol-name 8 string 9 otherwise 10 concatenate progn strip-cars syntaxp quotep assoc pairlis$ pairlis-x2 e/d 11 12 o-p o< acl2-count 13 let let* 14 cond case 15 and or not implies t nil quote 16 cons consp car cdr endp 17 list list* 18 atom symbolp natp 19 if equal 20 zp + - * / mod expt < <= > >=)) 21 22(begin-book t :ttags :all) 23|# 24 25(in-package "M1") 26 27; Problem Set 1 28 29; The bulk of this problem set asks you to define some ACL2 functions. I do 30; not particularly want you to use the mechanized version of ACL2 to check your 31; answers, but you are welcome to do so if you wish. If you do use the mechanized 32; system you will find that some of the function symbols I ask you to define are 33; already defined and the definitions are not always the ones I ask for below! 34; We will eventually learn how to use Common Lisp's ``package system'' to 35; avoid name conflicts; in the meanwhile, you can avoid name conflicts manually, 36; by choosing different names when you test your proposed definitions. 37 38; Answers should be typed and submitted by 3:30 pm Tuesday, Jan 23, 2007. To 39; submit your answers put all your answer files in a directory, myname-asgi, 40; where myname is your login name and i is the assignment number: 1, 2, .... 41; (Typically all your answers will be in a single file.) 42 43; Then execute on a CS Unix machine: 44 45; turnin --submit alexsp cs378 myname-asgi 46 47; To check your submissions: 48 49; turnin --list alexsp cs378 50 51; In my presentation of the problems below, when I write 52 53; expr ==> value 54 55; I mean that the expression expr evaluates to value. For example, 56 57; (+ 2 2) ==> 4. 58 59; In defining the required functions, limit yourself to the following 60; ACL2 forms and functions: 61 62; expression meaning 63 64; (defun fn (v1 ... vn) Define fn to take the formal arguments v1, ..., vn, 65; body) and to return the value of body (evaluated in an 66; environment where the vi are bound to the values 67; of the actuals). Thus, if I define 68; (defun sq (x) (* x x)) 69; then (sq 7) ==> 49. 70 71; (let ((v1 t1) Evaluate each of the ti. Then let the vi have those 72; ... respective values. In that environment, evaluate and 73; (vn tn)) return the value of body. 74; body) 75 76; (let* ((v1 t1) Evaluate t1 and let v1 have that value. Then ... 77; ... then evaluate tn and let vn have that value. In 78; (vn tn)) that environment, evaluate and return body. 79; body) 80 81; [Note: the difference between let and let* is that in the former the 82; variables get their values ``in parallel'' and in the latter they get them 83; ``in sequence.'' For example, suppose x has the value 1 in the ``global 84; environment.'' Then 85 86; (let ((x 5) (y (+ 1 x))) (* x y)) ==> 10 87 88; but 89 90; (let* ((x 5) (y (+ 1 x))) (* x y)) ==> 30 91 92; end of note] 93 94; (cond (p1 x1) Evaluate p1 and if non-nil, evaluate and return x1; 95; (p2 x2) else, evaluate p2 and if non-nil, evaluate and return x2; 96; ... ... 97; (t xk)) else, evaluate and return xk. 98 99; [Note: The cond above is just an abbreviation for 100; (if p1 x1 (if p2 x2 ... xk)).] 101 102; (case x Evaluate x and and if the value is literally 103; (sym1 y1) sym1, evaluate and return y1; else if the value is 104; (sym2 y2) sym2, evaluate and return y2; else if the value is 105; ... ... 106; (otherwise yk)) else, evaluate and return yk. 107 108; [Note: The symi MUST be symbols. Note that they are not evaluated! 109; The case above is just an abbreviation for: 110; (cond ((equal x 'sym1) y1) 111; ((equal x 'sym2) y2) 112; ... 113; (t yk)).] 114 115; (and p1 ... pn) t or nil depending on whether all the pi are non-nil. 116 117; (or p1 ... pn) t or nil depending on whether at least one pi is non-nil. 118 119; (not p1) t if p1 is nil and nil if p1 is t. 120 121; (implies p1 p2) t if either p1 is nil or p2 is t. 122 123; [Note: The descriptions above are right only if the pi are Boolean valued. 124; If the pi can return values other than t or nil, the descriptions are more 125; complicated. I recommend not testing non-Boolean expressions!] 126 127; (cons x y) the ordered pair whose left component (car) is x and 128; whose right component (cdr) is y 129 130; (consp x) t or nil indicating whether x is an ordered pair 131 132; (car x) the left component of the ordered pair x; or 133; nil if x is not an ordered pair. 134 135; (cdr x) the right component of the ordered pair x; or 136; nil if x is not an ordered pair. 137 138; (list x1 ... xn) same as (cons x1 (cons x2 ... (cons xn nil))) 139 140; (list* x1 ... xn) same as (cons x1 (cons x2 ... (cons xn-1 xn))) 141 142; (endp x) same as (not (consp x)) 143 144; (atom x) same as (not (consp x)) 145 146; (symbolp x) t or nil indicating whether x is a symbol 147 148; (keywordp x) t or nil indicating whether x is a keyword symbol 149 150; (natp x) t or nil indicating whether x is a natural number 151; (nonnegative integer) 152 153; (if x y z) if x is t, then y, else z; 154 155; [Note: The description is more complicated if x is not Boolean.] 156 157; (equal x y) t or nil indicating whether x and y are the same 158 159; (zp x) t or nil indicating whether x is 0 or not a natural 160; number. Thus, (zp -3) ==> t. 161 162; (+ x1 ... xn) sum of the xi 163 164; (* x1 ... xn) product of the xi 165 166; (- x1 x2) difference of x1 take away x2 167 168; (/ x1 x2) rational quotient of x1 divided by x2 169 170; (mod x1 x2) x1 mod x2, e.g., (mod 23 3) ==> 2 171 172; (expt x1 x2) x1 raised to the power x2 173 174; (< x1 x2) t or nil indicating whether x1 is less than x2 175 176; (<= x1 x2) t or nil indicating whether x1 is less than or 177; equal to x2 178 179; (> x1 x2) t or nil indicating whether x1 is greater than x2 180 181; (>= x1 x2) t or nil indicating whether x1 is greater than or 182; equal to x2 183 184; [Note: In the arithmetic functions, if an xi is not a number then it 185; is defaulted to 0. Thus (+ T 5) ==> 5.] 186 187; The way we will eventually implement this restriction to certain symbols is 188; to define the \ptt{"M1"} package to import the symbols above but not to 189; import certain other symbols -- namely the ones I'm asking you to define. 190 191; Recall from the lecture: 192 193(defun push (x y) (cons x y)) 194 195; | | 196; | cons in the ACL2 package 197; | 198; push in the M1 package 199 200; Thus, (push 3 nil) ==> (3) 201; (push 2 (push 3 nil)) ==> (2 3) 202; (push 1 (push 2 (push 3 nil))) ==> (1 2 3) 203 204; If we define top and pop like this: 205 206(defun top (stack) (car stack)) 207(defun pop (stack) (cdr stack)) 208 209; then (top (push 1 (push 2 (push 3 nil)))) ==> 1 210; (pop (push 1 (push 2 (push 3 nil)))) ==> (2 3) 211 212; A recursive definition: 213 214(defun nth (n list) 215 (if (zp n) 216 (car list) 217 (nth (- n 1) (cdr list)))) 218 219; Here is another handy definition: 220 221(defun make-state (pc locals stack program) 222 (cons pc 223 (cons locals 224 (cons stack 225 (cons program 226 nil))))) 227 228; Note: The cons nest above is the same thing as 229; (list pc locals stack program). 230 231(defun pc (s) (nth 0 s)) 232(defun locals (s) (nth 1 s)) 233(defun stack (s) (nth 2 s)) 234(defun program (s) (nth 3 s)) 235 236; ----------------------------------------------------------------- 237 238; Problem 1-1. ACL2 has various predicates for recognizing different kinds of Lisp 239; objects. Among them are: 240; a. NATP 241; b. STRINGP 242; c. CONSP 243; d. SYMBOLP 244; e. ENDP 245; f. KEYWORDP 246 247; Beside each object, indicate which of the above predicates it satisfies. 248 249; 1. 123 ((A - NATP) (E - ENDP)) 250; 2. ILOAD ((D - SYMBOLP) (E - ENDP)) 251; 3. INVOKEVIRTUAL ((D - SYMBOLP) (E - ENDP)) 252; 4. "Hello World!" ((B - STRINGP) (E - ENDP)) 253; 5. NIL ((D - SYMBOLP) (E - ENDP)) 254; 6. :NAME ((D - SYMBOLP) (E - ENDP) (F - KEYWORDP)) 255; 7. (ILOAD 0) ((C - CONSP)) 256; 8. ("Beta" "position") ((C - CONSP)) 257; 9. ((ILOAD 0) (IFNE 237)) ((C - CONSP)) 258; 10. ILOAD_0 ((D - SYMBOLP) (E - ENDP)) 259 260; --- 261 262; Problem 1-2. For each list x below, write down (CAR x), (CAR (CDR x)), and (CDR (CDR x)). 263 264; 1. (ILOAD 0) 265; Answers: ILOAD 0 NIL 266 267; 2. (GETFIELD ("Beta" "position")) 268; Answers: GETFIELD ("Beta" "position") NIL 269 270; 3. (IINC 3 -1) 271; Answers: IINC 3 (-1) 272 273; 4. (IADD) 274; Answers: IADD NIL NIL 275 276; 5. ((ILOAD 0) (IFNE 237) (ICONST_1)) 277; Answers: (ILOAD 0) (IFNE 237) ((ICONST_1)) 278 279; 6. (THREAD (:ID 3) (:CT NIL) (:STAT ACTIVE) (:REF (REF 27))) 280; Answers: THREAD (:ID 3) ((:CT NIL) (:STAT ACTIVE) (:REF (REF 27))) 281 282; 7. (:CT NIL) 283; Answers: :CT NIL NIL 284 285; --- 286 287; Problem 1-3. For each object below, write the CONS expression that constructs 288; it. Each answer will be a call of CONS, applied to numbers, quoted symbols, 289; strings, and/or NIL. 290 291; 0. (ILOAD 2) Answer: (cons 'ILOAD (cons 2 NIL)) 292 293; 1. (IADD) Answer: (cons 'IADD NIL) 294; 2. ((:ID 3) (:CT NIL)) 295; Answer: (cons (cons :ID (cons 3 nil)) 296; (cons (cons :CT (cons NIL nil)) 297; nil)) 298; 3. (NIL) Answer: (cons NIL nil) 299; 4. (GETFIELD ("Beta" "position")) 300; Answer: (cons 'GETFIELD 301; (cons (cons "Beta" (cons "position" nil)) 302; nil)) 303 304; --- 305 306; Problem 1-4: An ``instruction'' is a list of the form (op a1 ... ak), where 307; k=0, 1, 2, or 3. 308 309; Define opcode to take an instruction and return the op. Define arg1, arg2, 310; and arg3 to take an instruction and return the corresponding operand of the 311; instruction, or nil if it is not present. 312 313; Answer 1-4: 314 315(defun op-code (inst) (car inst)) 316(defun arg1 (inst) (nth 1 inst)) 317(defun arg2 (inst) (nth 2 inst)) 318(defun arg3 (inst) (nth 3 inst)) 319 320; --- 321 322; Problem 1-5: Fill in the blank: 323; (top (pop (push x (push y (push z nil))))) = ______________ 324 325; Answer 1-5: 326; (top (pop (push x (push y (push z nil))))) = y 327 328; --- 329 330; Problem 1-6: Can you PROVE your answer to Problem 1-5 is correct? 331 332; Answer 1-6: One way to prove this is to replace top, pop, and push by 333; their definitions and get 334 335; (car (cdr (cons x (cons y (cons z nil))))) = y 336 337; and then use the axioms for car-cons and cdr-cons. 338 339; A ``better'' way to prove it is to prove two lemmas (by following the scheme above 340; of replacing the stack functions by their definitions): 341 342; Lemma 1: top-push 343; (top (push x y)) = x 344 345; Lemma 2: pop-push 346; (pop (push x y)) = y 347 348; and then to apply those lemmas as follows: 349 350; Proof: 351; (top (pop (push x (push y (push z nil))))) 352; = {by Lemma 2 and replacement of equals by equals} 353; (top (push y (push z nil))) 354; = {by Lemma 1 and replacement of equals by equals} 355; y 356; Q.E.D. 357 358; --- 359 360; Problem 1-7: (stack (make-state a b c d)) = _____________ 361 362; Answer 1-7: (stack (make-state a b c d)) = c 363 364; --- 365 366; Problem 1-8: Prove Problem 1-7. 367 368; Answer 1-8: 369; Proof that (stack (make-state a b c d)) = c 370 371; (stack (make-state a b c d)) 372; = {def of stack} 373; (nth 2 (make-state a b c d)) 374; = {def nth and the facts (zp 2) = nil and (- 2 1) = 1 and basic axioms} 375; (nth 1 (cdr (make-state a b c d))) 376; = {def nth and the facts (zp 1) = nil and (- 1 1) = 0 and basic axioms} 377; (nth 0 (cdr (cdr (make-state a b c d)))) 378; = {defn nth and (zp 0) = t and basic axioms} 379; (car (cdr (cdr (make-state a b c d)))) 380; = {def make-state} 381; (car (cdr (cdr (cons a (cons b (cons c (cons d nil))))))) 382; = {basic axiom about cdr-cons} 383; (car (cdr (cons b (cons c (cons d nil))))) 384; = {basic axiom about cdr-cons} 385; (car (cons c (cons d nil))) 386; = {basic axiom about car-cons} 387; c 388; Q.E.D. 389 390; --- 391 392; Problem 1-9: 393; Define (len x) to return the number of elements of list x. 394; Thus, (len '(a b c)) ==> 3. (``==>'' means ``evaluates to'') 395 396; Answer 1-9: 397(defun len (x) 398 (if (endp x) 399 0 400 (+ 1 (len (cdr x))))) 401 402; --- 403 404; Problem 1-10: 405; Define (app x y) to concatenate two lists. 406; Thus, (app '(a b c) '(d e f)) ==> (A B C D E F). 407 408; Answer 1-10: 409(defun app (x y) 410 (if (endp x) 411 y 412 (cons (car x) 413 (app (cdr x) y)))) 414 415; --- 416 417; Problem 1-11: 418; Define (rev x) to reverse a list x. 419; Thus, (rev '(a b c)) ==> (C B A). 420 421; Answer 1-11: 422(defun rev (x) 423 (if (endp x) 424 nil 425 (app (rev (cdr x)) 426 (cons (car x) nil)))) 427 428; An alternative answer is the definition of frev below. 429 430(defun rev1 (x a) 431 (if (endp x) 432 a 433 (rev1 (cdr x) 434 (cons (car x) a)))) 435 436(defun frev (x) (rev1 x nil)) 437 438; --- 439 440; Problem 1-12: 441; Define (repeat x n) to return a list consisting of n 442; copies of x. Thus, (repeat 'a 5) ==> (A A A A A). 443 444; Answer 1-12: 445(defun repeat (th n) 446 (if (zp n) 447 nil 448 (cons th (repeat th (- n 1))))) 449 450; --- 451 452; Problem 1-13: 453; Define (popn n stk) to return the result of popping stk 454; n times. Thus, 455; (popn 2 (push 1 (push 2 (push 3 nil)))) ==> (3). 456 457; Answer 1-13: 458(defun popn (n stk) 459 (if (zp n) 460 stk 461 (popn (- n 1) (pop stk)))) 462 463; --- 464 465; Problem 1-14: 466; Define (update-nth n v x) so that the following is a 467; theorem 468; (implies (and (natp i) ; i is an integer and 0 <= i 469; (natp j)) 470; (equal (nth i (update-nth j v x)) 471; (if (equal i j) 472; v 473; (nth i x)))) 474 475; Answer 1-14: 476(defun update-nth (n v list) 477 (if (zp n) 478 (cons v (cdr list)) 479 (cons (car list) 480 (update-nth (- n 1) v (cdr list))))) 481 482; --- 483 484; Problem 1-15: 485; Define (member e lst) to return t or nil indicating 486; whether e is an element of list lst. 487; (member 3 '(1 2 3 4)) ==> T 488; (member 6 '(1 2 3 4)) ==> NIL 489 490; Answer 1-15: 491(defun member (e list) 492 (if (endp list) 493 nil 494 (if (equal e (car list)) 495 t 496 (member e (cdr list))))) 497 498; --- 499 500; Problem 1-16: 501; Define (index e x) so that the following is a theorem: 502; (implies (member e x) 503; (equal (nth (index e x) x) e)) 504 505; Answer 1-16: 506(defun index (e lst) 507 (if (endp lst) 508 0 509 (if (equal e (car lst)) 510 0 511 (+ 1 (index e (cdr lst)))))) 512 513; --- 514 515; Problem 1-17: 516; A ``keyword argument list'' is a list of even length whose even elements 517; (i.e., elements in the even positions, 0, 2, 4, ...) are keywords. Thus, 518; (:A 1 :B 2 :C 3) is a keyword argument list. So is (:A :B :B 2 :C 3). 519; We say that a value for keyword key is ``supplied'' by x if key appears 520; as an even element of x. Define (suppliedp key x) to return t or nil 521; to indicate whether key is supplied by x. 522 523; Answer 1-17: 524(defun suppliedp (key args) 525 (if (endp args) 526 nil 527 (if (equal key (car args)) 528 t 529 (suppliedp key (cdr (cdr args)))))) 530 531; --- 532 533; Problem 1-18: 534; If key is supplied by x, then its ``value'' is the element of x appearing 535; immediately after the first even occurrence of key in x. Define 536; (actual key x) to return the value of key in x, assuming key is supplied. 537 538; Answer 1-18: 539(defun actual (key args) 540 (if (endp args) 541 nil 542 (if (equal key (car args)) 543 (car (cdr args)) 544 (actual key (cdr (cdr args)))))) 545 546; --- 547 548; Problem 1-19: 549; A ``binding environment'' is a list of lists of the form 550; ((x1 y1) (x2 y2) ...). The xi are said to be the ``variables'' 551; and the yi are said to be their ``values.'' We say that a binding 552; environment ``binds'' x if x occurs as one of the xi. In that case, 553; x is said to ``bound'' and it is bound to the ``value'' y, where y is 554; (x y) is the first element in the environment binding x. 555 556; Define (boundp x env) to return T or NIL indicating whether x is bound 557; by binding environment env. 558 559; Answer 1-19: 560(defun boundp (var alist) 561 (if (endp alist) 562 nil 563 (if (equal var (car (car alist))) 564 t 565 (boundp var (cdr alist))))) 566 567; --- 568 569; Problem 1-20: 570; Define (binding x env) to return the value to which x is bound in binding 571; environment env, assuming x is bound. 572 573; Answer 1-20: 574(defun binding (var alist) 575 (if (endp alist) 576 nil 577 (if (equal var (car (car alist))) 578 (car (cdr (car alist))) 579 (binding var (cdr alist))))) 580 581; --- 582 583; Problem 1-21: 584; Define (bind x y env) so that the following is a theorem 585; (equal (binding v1 (bind v2 y env)) 586; (if (equal v1 v2) 587; y 588; (binding v1 env))) 589 590; Answer 1-21: 591(defun bind (var val alist) 592 (if (endp alist) 593 (cons (cons var (cons val nil)) nil) 594 (if (equal var (car (car alist))) 595 (cons (cons var (cons val nil)) (cdr alist)) 596 (cons (car alist) 597 (bind var val (cdr alist)))))) 598 599; Note: Here's another definition that works perfectly well. 600 601; (defun bind (var val alist) 602; (cons (cons var (cons val nil)) alist)) 603 604; --- 605 606; Problem 1-22: The ``unsigned n-bit interpretation'' of a natural number x is 607; the natural number denoted by the low order n bits of the binary 608; representation of k. Define (u-fix x n) to return the unsigned n-bit 609; interpretation of x. (The name ``u-fix'' stands for ``unsigned fix'' and 610; suggests the idea of converting (or ``fixing'') an arbitrary natural into a 611; particular format.) 612 613; Answer 1-22: 614(defun u-fix (x n) 615 (mod x (expt 2 n))) 616 617; --- 618 619; Problem 1-23: The ``signed n-bit interpretation'' of a natural number x is the 620; integer twos complement intepretation of the low order n bits of the binary 621; representation of k. The table below illustrates the signed 3-bit 622; interpretation of a range of naturals numbers x. 623 624; nat binary twos-complement 625; x integer 626 627; 0 000 0 628; 1 001 1 629; 2 010 2 630; 3 011 3 631; 4 100 -4 632; 5 101 -3 633; 6 110 -2 634; 7 111 -1 635; 8 1000 0 636; 9 1001 1 637;10 1010 2 638;11 1011 3 639;12 1100 -4 640;13 1101 -3 641;... ... ... 642 643; Define (s-fix x n) to return the signed n-bit interpretation of the natural 644; number x. 645 646; Answer 1-23: 647(defun s-fix (x n) 648 (let ((temp (mod x (expt 2 n)))) 649 (if (< temp (expt 2 (- n 1))) 650 temp 651 (- temp (expt 2 n))))) 652 653; --- 654 655; Problem 1-24: A ``byte'' is an integer b that can be represented in 8-bits, 656; e.g., (and (natp b) (< b 256)). A list of bytes can be thought of as an 657; unsighed base 256 ``big number'' in conventional ``big endian'' notation, 658; e.g., where the car of the list is the most significant ``digit.'' Thus, 659; (192 168 0 123) denotes the natural 3232235643, which is 660 661; (+ (* 192 (expt 256 3)) 662; (* 168 (expt 256 2)) 663; (* 0 (expt 256 1)) 664; (* 123 (expt 256 0))) 665 666; Define (u-big lst) to return the unsigned base 256 big endian interpretation 667; of the list of bytes lst. 668 669; Answer 1-24: 670(defun u-big1 (lst acc) 671 (if (endp lst) 672 acc 673 (u-big1 (cdr lst) 674 (+ (u-fix (car lst) 8) 675 (* (expt 2 8) acc))))) 676 677(defun u-big (lst) (u-big1 lst 0)) 678 679; --- 680 681; Problem 1-25: The ``signed base 256 big endian interpretation'' of a list of k 682; bytes is the 8*k twos-complement interpretation of the unsigned base 256 big 683; endian interpretation. Define (s-big lst) to return the signed base 256 big 684; endian interpretation of the list of bytes lst. 685 686; Answer 1-25: 687(defun s-big (lst) 688 (s-fix (u-big lst) (* 8 (len lst)))) 689 690; --- 691 692; Problem 1-26: Define (nextn n lst) to return the first n elements of the list 693; lst. You may assume that lst has at least n elements. Thus 694; (nextn 3 '(a b c d e)) ==> (A B C) 695 696; Answer 1-26: 697(defun nextn (n lst) 698 (if (zp n) 699 nil 700 (cons (car lst) 701 (nextn (- n 1) (cdr lst))))) 702 703; --- 704 705; Problem 1-27: Define (skipn n lst) to return the result of removing the first n 706; elements from lst. You may assume that lst has at least n elements. Thus, 707; (skipn 3 '(a b c d e)) ==> (D E). 708 709; Answer 1-27: 710(defun skipn (n lst) 711 (if (zp n) 712 lst 713 (skipn (- n 1) (cdr lst)))) 714 715; --- the end --- 716 717