← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2009/cowles-gamboa-triangle-square/materials/Readme.lsp

  • 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/2009/cowles-gamboa-triangle-square/materials/Readme.lsp
 
1
((:FILES ; non-empty list of filenames, generated from Unix command "ls -1R"
 
2
"
 
3
 .:
 
4
 Readme.lsp
 
5
 tri-sq.lisp
 
6
 log2.lisp
 
7
 
 
8
")
 
9
(:TITLE    "Solving TRIANGLE = SQUARE")
 
10
(:AUTHOR/S "John R. Cowles"
 
11
           "Ruben Gamboa") 
 
12
(:KEYWORDS "triangular numbers" 
 
13
           "Pell's equation"
 
14
           "Log base 2"
 
15
           "Floor Log base 2"
 
16
           "Ceiling Log base 2")
 
17
(:ABSTRACT 
 
18
 "For positive integer n, the triangular number, Delta_n, is defined by
 
19
      Delta_n = 1 + 2 + ... + (n-1) + n
 
20
              = n * (n + 1) / 2.
 
21
  The first 6 triangular numbers are Delta_1 = 1, Delta_2 = 3,
 
22
  Delta_3 = 6, Delta_4 = 10, Delta_5 = 15, and Delta_6 = 21.
 
23
 
 
24
  Problem. Find triangular numbers that are also squares.
 
25
           That is, find positive integers, n and k, such that
 
26
                    n * (n + 1) / 2 = k^2
 
27
                  or
 
28
                    n * (n + 1) = 2 * k^2.
 
29
 
 
30
  Clearly Delta_1 = 1 is a square. Are there other square triangular numbers?
 
31
  Are there infinitely many square triangular numbers?  These questions are
 
32
  answered below and the answers are formally verfied using ACL2.
 
33
  
 
34
  Define functions that compute floor of log base 2 and
 
35
  ceiling log base 2 for nonnegative integers n.
 
36
 
 
37
  Show these functions are correct.
 
38
  Show these functions use logarithmic number, in input n, 
 
39
  of arithmetic operations to compute their results.") 
 
40
(:PERMISSION ; author/s permission for distribution and copying:
 
41
 "ACL2 book Solving TRIANGLE = SQUARE
 
42
  Copyright (C) 2008 John R. Cowles and Ruben Gamboa, University of Wyoming
 
43
 
 
44
  This book is free software; you can redistribute it and/or
 
45
  modify it under the terms of the GNU General Public License
 
46
  as published by the Free Software Foundation; either version 2
 
47
  of the License, or (at your option) any later version.
 
48
 
 
49
  This book is distributed in the hope that it will be useful,
 
50
  but WITHOUT ANY WARRANTY; without even the implied warranty of
 
51
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
52
  GNU General Public License for more details.
 
53
 
 
54
  You should have received a copy of the GNU General Public License
 
55
  along with this book; if not, write to the Free Software
 
56
  Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
 
57
  02110-1301, USA."))
 
 
b'\\ No newline at end of file'