---

4.2 Homework 1

                        Homework Assignment 1
                               CS 389r
                         Unique Number: 53119
                             Fall, 2021

                       Given:  September   7, 2021
                        Due:   September 16, 2021

This assignment is based on the material from Moore’s Recursion and Induction notes. Please read the first six sections before attempting to do the homework.

Part 1:

Part 1 of your homework assignment is to provide solutions for problems 6 – 17.

Part 2:

We will be using the ACL2 theorem-proving system starting in a couple of weeks. The top-level ACL2 webpage can be found here:

http://www.cs.utexas.edu/users/moore/acl2/

If you wish to use this system on UTCS Linux-based computers, then be sure that you have appropriate usage privileges. Once you have logged into a UTCS Linux-based computer, then you may type:

/p/bin/acl2

at the unix system prompt to start ACL2 running. If you wish to use ACL2 on your personal laptop, then you will need to follow the ACL2 installation instructions which can be found here:

http://www.cs.utexas.edu/users/moore/acl2/v7-0/HTML/installation/installation.html

Before ACL2 can be built on your laptop or deskside computer, you will need to obtain a Lisp implementation. We strongly recommend that you use Clozure Common Lisp. Why? This is the Lisp that we generally use. This hashtag contains a bit of information that might be helpful.

http://www.cs.utexas.edu/users/moore/acl2/v7-0/HTML/installation/requirements.html#Obtaining-CCL

Part 2 of your homework assignment is to provide us with a copy of the ACL2 welcome header you see when you run the command to start-up ACL2 on the computer you will be using for ACL2 assignments this semester. It should look something like this...

sms@Scott-MacBook-Pro ccl-acl2-8.3 % ./saved_acl2

Welcome to Clozure Common Lisp Version 1.12 (v1.12-32-g8778079b) DarwinX8664!

 ACL2 Version 8.3 built December 3, 2020  06:05:40.
 Copyright (C) 2020, Regents of the University of Texas
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the LICENSE file distributed with ACL2.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
 See the documentation topic note-8-3 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

ACL2 Version 8.3.  Level 1.  Cbd "/Users/sms/acl2/ccl-acl2-8.3/".
System books directory "/Users/sms/acl2/ccl-acl2-8.3/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

;;;
;;; Quick test of defining a recursive function in ACL2
;;;
ACL2 !> (defun sum-to-n (n)
              (if (zp n) ; Is n zero?
                 0
               (+ n
                  (sum-to-n (1- n)))))

The admission of SUM-TO-N is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT N).  We observe that the type of SUM-TO-N is described
by the theorem (AND (INTEGERP (SUM-TO-N N)) (<= 0 (SUM-TO-N N))). 
We used the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive
type reasoning.

Summary
Form:  ( DEFUN SUM-TO-N ...)
Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 SUM-TO-N
ACL2 !> (good-bye)

sms@Scott-MacBook-Pro ccl-acl2-8.3 % 

NOTE: If you have any trouble getting access to ACL2 on the UTCS Linux machines, or difficulty in installing and running ACL2 on your personal machine, see Professor Hunt or one of his staff immediately. You cannot do the work for this class without this software system available to you.