Next: Homework 2, Previous: Homework 0, Up: CS389r Homework [Contents][Index]
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.
Next: Homework 2, Previous: Homework 0, Up: CS389r Homework [Contents][Index]