← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/1999/knuth-91/exercise2.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/1999/knuth-91/exercise2.lisp
 
1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
2
;; John Cowles,
 
3
;; Knuth's Generalization of McCarthy's 91 Function.
 
4
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
5
;;Exercise 2.
 
6
;; Part A.
 
7
 
 
8
;; Formally state McCarthy's definition for the 91 function in 
 
9
;; ACL2:
 
10
 
 
11
;;   M(x) <==  if  x > 100  then   x - 10
 
12
;;                          else   M(M(x+11)).
 
13
 
 
14
;; Use the following proposed measure:
 
15
 
 
16
;;   measure(x) <==  if   x > 100  then  0
 
17
;;                                 else  101 - x.
 
18
 
 
19
;; Observe ACL2's resistance to accepting this definition.  
 
20
;; Carefully note the non-trivial part of the measure conjecture.
 
21
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
22
;;Answer.
 
23
;; Submit the following to a newly started ACL2:
 
24
 
 
25
(in-package "ACL2") ; in order to certify this book
 
26
 
 
27
(defun
 
28
    measure (x)
 
29
    (if (> x 100)
 
30
        0
 
31
        (- 101 x)))
 
32
 
 
33
#|
 
34
(defun
 
35
    M (x)
 
36
    ;; Fails -- Study the measure conjecture.
 
37
    (declare (xargs :measure (measure x)))
 
38
    (if (> x 100)
 
39
        (- x 10)
 
40
        (M (M (+ x 11)))))
 
41
|#
 
42
 
 
43
;;Some output from ACL2:
 
44
 
 
45
;; The non-trivial part of the measure conjecture is
 
46
 
 
47
;; Goal
 
48
;; (AND (E0-ORDINALP (MEASURE X))
 
49
;;      (IMPLIES (<= X 100)
 
50
;;               (E0-ORD-< (MEASURE (+ X 11))
 
51
;;                         (MEASURE X)))
 
52
;;      (IMPLIES (<= X 100)
 
53
;;               (E0-ORD-< (MEASURE (M (+ X 11)))
 
54
;;                         (MEASURE X)))).
 
55
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
56
;;Exercise 2.
 
57
;; Part B.
 
58
 
 
59
;; Formally state the following definition in ACL2:
 
60
 
 
61
;;  M(x) <==  if   x > 100  then  x - 10 
 
62
;;                          else  91.
 
63
 
 
64
;; Observe that ACL2 accepts this definition. Next, formally state
 
65
;; and prove, in ACL2, that the next equation holds for all 
 
66
;; integers x.
 
67
 
 
68
;;   M(x)  =  if  x > 100  then  x - 10 
 
69
;;                         else  M(M(x+11)).
 
70
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
71
;;Answer.
 
72
;; Submit the following to a newly started ACL2:
 
73
 
 
74
(defun
 
75
    M (x)
 
76
    ;; Equation 1.3
 
77
    (if (> x 100)
 
78
        (- x 10)
 
79
        91))
 
80
 
 
81
(defthm
 
82
    Equation-1.4
 
83
    (implies (integerp x)
 
84
             (equal (M x)
 
85
                    (if (> x 100)
 
86
                        (- x 10)
 
87
                        (M (M (+ x 11)))))))