# Author: Paul Fitzpatrick, paulfitz@csail.mit.edu
# Copyright (c) 2005 Paul Fitzpatrick
#
# This file is part of CosmicOS.
#
# CosmicOS is free software; you can redistribute it and / or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# CosmicOS is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with CosmicOS; if not, write to the Free Software
# Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
#
# MATH introduce numbers (in unary notation)
# Here we count up, go through some primes, etc.
# There is some syntax around the numbers, but that doesn't
# need to be understood at this point.
# Any 'words' written here are converted to arbitrary integers
# in the actual message. Any word ending in -in-unary will be given
# in unary rather than the binary code used in the main body
# of the message.
[hear] (intro-in-unary 010);
[hear] (intro-in-unary 0110);
[hear] (intro-in-unary 01110);
[hear] (intro-in-unary 011110);
[hear] (intro-in-unary 0111110);
[hear] (intro-in-unary 01111110);
[hear] (intro-in-unary 011111110);
[hear] (intro-in-unary 0111111110);
[hear] (intro-in-unary 01111111110);
[hear] (intro-in-unary 011111111110);
[hear] (intro-in-unary 0111111111110);
[hear] (intro-in-unary 01111111111110);
[hear] (intro-in-unary 011111111111110);
[hear] (intro-in-unary 0111111111111110);
[hear] (intro-in-unary 01111111111111110);
[hear] (intro-in-unary 011111111111111110);
[hear] (intro-in-unary 0110);
[hear] (intro-in-unary 01110);
[hear] (intro-in-unary 0111110);
[hear] (intro-in-unary 011111110);
[hear] (intro-in-unary 0111111111110);
[hear] (intro-in-unary 011111111111110);
[hear] (intro-in-unary 010);
[hear] (intro-in-unary 011110);
[hear] (intro-in-unary 01111111110);
[hear] (intro-in-unary 011111111111111110);
# MATH introduce equality for unary numbers
# The intro operator does nothing essential, and could be
# omitted - it just tags the first use of a new operator.
# The = operator is introduced alongside a duplication of
# unary numbers. The meaning will not quite by nailed down
# until we see other relational operators.
[hear] (=-in-unary 010 010);
[hear] (=-in-unary 0110 0110);
[hear] (=-in-unary 01110 01110);
[hear] (=-in-unary 011110 011110);
[hear] (=-in-unary 0111110 0111110);
[hear] (=-in-unary 01111110 01111110);
[hear] (=-in-unary 011111110 011111110);
[hear] (=-in-unary 0111111110 0111111110);
[hear] (=-in-unary 010 010);
[hear] (=-in-unary 01111110 01111110);
[hear] (=-in-unary 0110 0110);
# MATH now introduce other relational operators
# After this lesson, it should be clear what contexts
# < > and = are appropriate in.
# drive the lesson home
[hear] (=-in-unary 010 010);
[hear] (>-in-unary 0110 010);
[hear] (>-in-unary 01110 010);
[hear] (>-in-unary 011110 010);
[hear] (<-in-unary 010 0110);
[hear] (=-in-unary 0110 0110);
[hear] (>-in-unary 01110 0110);
[hear] (>-in-unary 011110 0110);
[hear] (<-in-unary 010 01110);
[hear] (<-in-unary 0110 01110);
[hear] (=-in-unary 01110 01110);
[hear] (>-in-unary 011110 01110);
[hear] (<-in-unary 010 011110);
[hear] (<-in-unary 0110 011110);
[hear] (<-in-unary 01110 011110);
[hear] (=-in-unary 011110 011110);
[hear] (>-in-unary 010 00);
[hear] (>-in-unary 01111111110 0110);
[hear] (>-in-unary 01111110 00);
[hear] (>-in-unary 0110 00);
[hear] (>-in-unary 0111111110 0110);
[hear] (>-in-unary 011110 010);
[hear] (>-in-unary 0110 00);
[hear] (>-in-unary 011111111110 010);
[hear] (>-in-unary 01111110 010);
[hear] (>-in-unary 01111111110 010);
[hear] (>-in-unary 011111110 010);
[hear] (<-in-unary 00 010);
[hear] (<-in-unary 01110 011111111110);
[hear] (<-in-unary 011110 01111111110);
[hear] (<-in-unary 0110 011110);
[hear] (<-in-unary 010 011111110);
[hear] (<-in-unary 00 011111111110);
[hear] (<-in-unary 00 0110);
[hear] (<-in-unary 00 0110);
[hear] (<-in-unary 010 01110);
[hear] (<-in-unary 0110 0111110);
[hear] (<-in-unary 010 011110);
# switch to binary labelling for commands
[hear] (= 010 010);
[hear] (> 0110 010);
[hear] (> 01110 010);
[hear] (> 011110 010);
[hear] (< 010 0110);
[hear] (= 0110 0110);
[hear] (> 01110 0110);
[hear] (> 011110 0110);
[hear] (< 010 01110);
[hear] (< 0110 01110);
[hear] (= 01110 01110);
[hear] (> 011110 01110);
[hear] (< 010 011110);
[hear] (< 0110 011110);
[hear] (< 01110 011110);
[hear] (= 011110 011110);
# a few more random examples
[hear] (< 01110 011110);
[hear] (= 011110 011110);
[hear] (< 010 0111110);
[hear] (> 011110 00);
[hear] (> 0111110 011110);
[hear] (< 0110 01110);
[hear] (> 0110 010);
[hear] (> 0111110 010);
[hear] (= 01110 01110);
[hear] (= 01110 01110);
[hear] (> 010 00);
# MATH introduce the NOT logical operator
[hear] (intro not);
[hear] (= 00 00);
[hear] (not / < 00 00);
[hear] (not / > 00 00);
[hear] (= 011110 011110);
[hear] (not / < 011110 011110);
[hear] (not / > 011110 011110);
[hear] (= 01111110 01111110);
[hear] (not / < 01111110 01111110);
[hear] (not / > 01111110 01111110);
[hear] (= 0110 0110);
[hear] (not / < 0110 0110);
[hear] (not / > 0110 0110);
[hear] (= 01110 01110);
[hear] (not / < 01110 01110);
[hear] (not / > 01110 01110);
[hear] (not / = 01110 011111111110);
[hear] (< 01110 011111111110);
[hear] (not / > 01110 011111111110);
[hear] (not / = 0111110 011111110);
[hear] (< 0111110 011111110);
[hear] (not / > 0111110 011111110);
[hear] (not / = 010 0110);
[hear] (< 010 0110);
[hear] (not / > 010 0110);
[hear] (not / = 00 0111110);
[hear] (< 00 0111110);
[hear] (not / > 00 0111110);
[hear] (not / = 0111111110 0111111111111110);
[hear] (< 0111111110 0111111111111110);
[hear] (not / > 0111111110 0111111111111110);
[hear] (not / = 0111111111110 01111110);
[hear] (> 0111111111110 01111110);
[hear] (not / < 0111111111110 01111110);
[hear] (not / = 01111111111110 0110);
[hear] (> 01111111111110 0110);
[hear] (not / < 01111111111110 0110);
[hear] (not / = 011111111110 011111110);
[hear] (> 011111111110 011111110);
[hear] (not / < 011111111110 011111110);
[hear] (not / = 011110 00);
[hear] (> 011110 00);
[hear] (not / < 011110 00);
[hear] (not / = 011111111111111110 01111111110);
[hear] (> 011111111111111110 01111111110);
[hear] (not / < 011111111111111110 01111111110);
# MATH introduce addition
[hear] (intro +);
[hear] (= 0110 / + 00 0110);
[hear] (= 0111110 / + 011110 010);
[hear] (= 0110 / + 0110 00);
[hear] (= 011110 / + 00 011110);
[hear] (= 011110 / + 01110 010);
[hear] (= 01110 / + 010 0110);
[hear] (= 00 / + 00 00);
[hear] (= 011110 / + 011110 00);
[hear] (= 01110 / + 0110 010);
[hear] (= 011110 / + 011110 00);
# MATH introduce subtraction
[hear] (intro -);
[hear] (= 00 / - 0110 0110);
[hear] (= 011110 / - 0111110 010);
[hear] (= 0110 / - 0110 00);
[hear] (= 00 / - 011110 011110);
[hear] (= 01110 / - 011110 010);
[hear] (= 010 / - 01110 0110);
[hear] (= 00 / - 00 00);
[hear] (= 011110 / - 011110 00);
[hear] (= 0110 / - 01110 010);
[hear] (= 011110 / - 011110 00);
# MATH introduce multiplication
[hear] (intro *);
[hear] (= 00 / * 00 00);
[hear] (= 00 / * 00 010);
[hear] (= 00 / * 00 0110);
[hear] (= 00 / * 00 01110);
[hear] (= 00 / * 010 00);
[hear] (= 010 / * 010 010);
[hear] (= 0110 / * 010 0110);
[hear] (= 01110 / * 010 01110);
[hear] (= 00 / * 0110 00);
[hear] (= 0110 / * 0110 010);
[hear] (= 011110 / * 0110 0110);
[hear] (= 01111110 / * 0110 01110);
[hear] (= 00 / * 01110 00);
[hear] (= 01110 / * 01110 010);
[hear] (= 01111110 / * 01110 0110);
[hear] (= 01111111110 / * 01110 01110);
[hear] (= 00 / * 00 010);
[hear] (= 01110 / * 01110 010);
[hear] (= 00 / * 0110 00);
[hear] (= 00 / * 00 01110);
[hear] (= 01110 / * 01110 010);
[hear] (= 0110 / * 010 0110);
[hear] (= 00 / * 00 00);
[hear] (= 00 / * 01110 00);
[hear] (= 00 / * 0110 00);
[hear] (= 00 / * 01110 00);
# MATH introduce a simple form of binary notation
# After this lesson, in the higher-level version of the message,
# will expand decimal to stand for the binary notation given.
# It wouldn't be hard to accompany this lesson with a more
# formal definition once functions are introduced (below)
# so maybe the transition to binary should be delayed?
[hear] (= (:) 010);
[hear] (= (:.) 0110);
[hear] (= (:..) 011110);
[hear] (= (:...) 0111111110);
[hear] (= (:....) 011111111111111110);
[hear] (= (.) 00);
[hear] (= (:) 010);
[hear] (= (:.) 0110);
[hear] (= (::) 01110);
[hear] (= (:..) 011110);
[hear] (= (:.:) 0111110);
[hear] (= (::.) 01111110);
[hear] (= (:::) 011111110);
[hear] (= (:...) 0111111110);
[hear] (= (:..:) 01111111110);
[hear] (= (:.:.) 011111111110);
[hear] (= (:.::) 0111111111110);
[hear] (= (::..) 01111111111110);
[hear] (= (::.:) 011111111111110);
[hear] (= (:::.) 0111111111111110);
[hear] (= (::::) 01111111111111110);
[hear] (= (.) 00);
[hear] (= (:::) 011111110);
[hear] (= (::.:) 011111111111110);
[hear] (= (:.:) 0111110);
[hear] (= (:..:) 01111111110);
[hear] (= (.) 00);
[hear] (= (::) 01110);
[hear] (= (::::) 01111111111111110);
[hear] (= (::..) 01111111111110);
[hear] (= (:.:) 0111110);
[hear] (= (:.:) 0111110);
[hear] (= (:..:) 01111111110);
[hear] (= (:.) 0110);
[hear] (= (:) 010);
[hear] (= (::::) 01111111111111110);
[hear] (= (:.) 0110);
[hear] (= 0111110 / + 011110 010);
[hear] (= (:.:) / + (:..) (:));
[hear] (= 011111110 / + 01111110 010);
[hear] (= (:::) / + (::.) (:));
[hear] (= 0111110 / + 011110 010);
[hear] (= (:.:) / + (:..) (:));
[hear] (= 011110 / + 00 011110);
[hear] (= (:..) / + (.) (:..));
[hear] (= 01111111110 / + 011111110 0110);
[hear] (= (:..:) /
+ (:::) (:.));
[hear] (= 0111111111110 / + 011111110 011110);
[hear] (= (:.::) /
+ (:::) (:..));
[hear] (= 011111111110 / + 01110 011111110);
[hear] (= (:.:.) /
+ (::) (:::));
[hear] (= 01111110 / + 0111110 010);
[hear] (= (::.) / + (:.:) (:));
[hear] (= 011110 / * 011110 010);
[hear] (= (:..) / * (:..) (:));
[hear] (= 011110 / * 010 011110);
[hear] (= (:..) / * (:) (:..));
[hear] (= 011110 / * 010 011110);
[hear] (= (:..) / * (:) (:..));
[hear] (= 01111110 / * 0110 01110);
[hear] (= (::.) / * (:.) (::));
[hear] (= 01111110 / * 0110 01110);
[hear] (= (::.) / * (:.) (::));
[hear] (= 011110 / * 0110 0110);
[hear] (= (:..) / * (:.) (:.));
[hear] (= 01111111110 / * 01110 01110);
[hear] (= (:..:) /
* (::) (::));
[hear] (= 011111111111111110 / * 011110 011110);
[hear] (= (:....) /
* (:..) (:..));
# MATH show local assignment
[hear] (assign 20 0 / = (20) 0);
[hear] (assign 20 1 / = (20) 1);
[hear] (assign 20 2 / = (20) 2);
[hear] (assign 21 0 / = (21) 0);
[hear] (assign 21 1 / = (21) 1);
[hear] (assign 21 2 / = (21) 2);
[hear] (assign 22 0 / = (22) 0);
[hear] (assign 22 1 / = (22) 1);
[hear] (assign 22 2 / = (22) 2);
[hear] (= 0 (assign 20 0 (20)));
[hear] (= 0 (assign 20 0 / 20));
[hear] (= 0 / assign 20 0 / 20);
[hear] (= 20 / assign 20 0 20);
[hear] (= 5 / assign 20 0 5);
[hear] (= 5 / assign 20 0 / assign 23 5 / 23);
[hear] (= 23 / assign 20 0 / assign 23 5 23);
[hear] (= 1 (assign 20 1 (20)));
[hear] (= 1 (assign 20 1 / 20));
[hear] (= 1 / assign 20 1 / 20);
[hear] (= 20 / assign 20 1 20);
[hear] (= 5 / assign 20 1 5);
[hear] (= 5 / assign 20 1 / assign 23 5 / 23);
[hear] (= 23 / assign 20 1 / assign 23 5 23);
[hear] (= 2 (assign 20 2 (20)));
[hear] (= 2 (assign 20 2 / 20));
[hear] (= 2 / assign 20 2 / 20);
[hear] (= 20 / assign 20 2 20);
[hear] (= 5 / assign 20 2 5);
[hear] (= 5 / assign 20 2 / assign 23 5 / 23);
[hear] (= 23 / assign 20 2 / assign 23 5 23);
[hear] (= 0 (assign 21 0 (21)));
[hear] (= 0 (assign 21 0 / 21));
[hear] (= 0 / assign 21 0 / 21);
[hear] (= 21 / assign 21 0 21);
[hear] (= 5 / assign 21 0 5);
[hear] (= 5 / assign 21 0 / assign 23 5 / 23);
[hear] (= 23 / assign 21 0 / assign 23 5 23);
[hear] (= 1 (assign 21 1 (21)));
[hear] (= 1 (assign 21 1 / 21));
[hear] (= 1 / assign 21 1 / 21);
[hear] (= 21 / assign 21 1 21);
[hear] (= 5 / assign 21 1 5);
[hear] (= 5 / assign 21 1 / assign 23 5 / 23);
[hear] (= 23 / assign 21 1 / assign 23 5 23);
[hear] (= 2 (assign 21 2 (21)));
[hear] (= 2 (assign 21 2 / 21));
[hear] (= 2 / assign 21 2 / 21);
[hear] (= 21 / assign 21 2 21);
[hear] (= 5 / assign 21 2 5);
[hear] (= 5 / assign 21 2 / assign 23 5 / 23);
[hear] (= 23 / assign 21 2 / assign 23 5 23);
[hear] (= 0 (assign 22 0 (22)));
[hear] (= 0 (assign 22 0 / 22));
[hear] (= 0 / assign 22 0 / 22);
[hear] (= 22 / assign 22 0 22);
[hear] (= 5 / assign 22 0 5);
[hear] (= 5 / assign 22 0 / assign 23 5 / 23);
[hear] (= 23 / assign 22 0 / assign 23 5 23);
[hear] (= 1 (assign 22 1 (22)));
[hear] (= 1 (assign 22 1 / 22));
[hear] (= 1 / assign 22 1 / 22);
[hear] (= 22 / assign 22 1 22);
[hear] (= 5 / assign 22 1 5);
[hear] (= 5 / assign 22 1 / assign 23 5 / 23);
[hear] (= 23 / assign 22 1 / assign 23 5 23);
[hear] (= 2 (assign 22 2 (22)));
[hear] (= 2 (assign 22 2 / 22));
[hear] (= 2 / assign 22 2 / 22);
[hear] (= 22 / assign 22 2 22);
[hear] (= 5 / assign 22 2 5);
[hear] (= 5 / assign 22 2 / assign 23 5 / 23);
[hear] (= 23 / assign 22 2 / assign 23 5 23);
# Now for functions.
[hear] (assign 20 (? 28 5) / = 5 (20 2));
[hear] (assign 32 (? 24 5) / = 5 (32 3));
[hear] (assign 28 (? 29 6) / = 6 (28 2));
[hear] (assign 30 (? 32 6) / = 6 (30 3));
[hear] (assign 25 (? 38 (38)) / = 2 (25 2));
[hear] (assign 23 (? 30 (30)) / = 3 (23 3));
[hear] (assign 25 (? 33 (33)) / = 2 (25 2));
[hear] (assign 29 (? 21 (21)) / = 3 (29 3));
[hear] (assign 25 (? 32 / + (32) 1) / = 3 (25 2));
[hear] (assign 31 (? 38 / + (38) 1) / = 4 (31 3));
[hear] (assign 35 (? 33 / + (33) 1) / = 3 (35 2));
[hear] (assign 32 (? 26 / + (26) 1) / = 4 (32 3));
[hear] (assign y (? x / + (x) 6) / = (y 6) 12);
[hear] (= ((? x / + (x) 6) 6) 12);
[hear] (assign y (? x / + (x) 4) / = (y 0) 4);
[hear] (= ((? x / + (x) 4) 0) 4);
[hear] (assign y (? x / + (x) 12) / = (y 0) 12);
[hear] (= ((? x / + (x) 12) 0) 12);
[hear] (assign y (? x / + (x) 15) / = (y 2) 17);
[hear] (= ((? x / + (x) 15) 2) 17);
[hear] (assign z (? x / ? y / + 1 / * (x) (y)) /
= (z 13 4) 53);
[hear] (assign z (? x / ? y / + 1 / * (x) (y)) /
= ((z 13) 4) 53);
[hear] (= ((? x / ? y / + 1 / * (x) (y)) 13 4) 53);
[hear] (= (((? x / ? y / + 1 / * (x) (y)) 13) 4)
53);
[hear] (assign z (? x / ? y / + 1 / * (x) (y)) /
= (z 5 6) 31);
[hear] (assign z (? x / ? y / + 1 / * (x) (y)) /
= ((z 5) 6) 31);
[hear] (= ((? x / ? y / + 1 / * (x) (y)) 5 6) 31);
[hear] (= (((? x / ? y / + 1 / * (x) (y)) 5) 6)
31);
[hear] (assign z (? x / ? y / + 1 / * (x) (y)) /
= (z 7 8) 57);
[hear] (assign z (? x / ? y / + 1 / * (x) (y)) /
= ((z 7) 8) 57);
[hear] (= ((? x / ? y / + 1 / * (x) (y)) 7 8) 57);
[hear] (= (((? x / ? y / + 1 / * (x) (y)) 7) 8)
57);
[hear] (assign z (? x / ? y / + 1 / * (x) (y)) /
= (z 8 2) 17);
[hear] (assign z (? x / ? y / + 1 / * (x) (y)) /
= ((z 8) 2) 17);
[hear] (= ((? x / ? y / + 1 / * (x) (y)) 8 2) 17);
[hear] (= (((? x / ? y / + 1 / * (x) (y)) 8) 2)
17);
[hear] (assign
w
(? x /
? y /
? z /
= (z) /
+ (x) (y)) /
w 15 14 29);
[hear] (assign
w
(? x /
? y /
? z /
= (z) /
+ (x) (y)) /
w 5 8 13);
[hear] (assign
w
(? x /
? y /
? z /
= (z) /
+ (x) (y)) /
w 12 15 27);
[hear] (assign
w
(? x /
? y /
? z /
= (z) /
+ (x) (y)) /
w 14 14 28);
[hear] (assign
w
(? x /
? y /
? z /
= (z) /
+ (x) (y)) /
w 8 0 8);
[hear] (assign
w
(? x /
? y /
? z /
= (z) /
+ (x) (y)) /
w 15 9 24);
[hear] (assign
w
(? x /
? y /
? z /
= (z) /
+ (x) (y)) /
w 11 15 26);
[hear] (assign
w
(? x /
? y /
? z /
= (z) /
+ (x) (y)) /
w 5 7 12);
# MATH demonstrate existence of memory
[hear] (define forty-something 42);
[hear] (= 42 (forty-something));
# now introduce a function
[hear] (assign square (? x / * (x) (x)) /
= 0 (square 0));
[hear] (assign square (? x / * (x) (x)) /
= 16 (square 4));
[hear] (assign square (? x / * (x) (x)) /
= 64 (square 8));
[hear] (assign square (? x / * (x) (x)) /
= 9 (square 3));
# show that functions can be remembered across statements
[hear] (define square / ? x / * (x) (x));
[hear] (= (square 5) 25);
[hear] (= (square 0) 0);
[hear] (= (square 1) 1);
[hear] (= (square 9) 81);
[hear] (define plusone / ? x / + (x) 1);
[hear] (= (plusone 7) 8);
[hear] (= (plusone 3) 4);
[hear] (= (plusone 3) 4);
[hear] (= (plusone 5) 6);
# This could all be simplified or removed
# once the handling of true / false stabilizes
# MATH use equality for truth values
[hear] (= (= 0110 0110) (> 011110 0110));
[hear] (= (= 010 010) (> 01111110 011110));
[hear] (= (< 01110 011110) (= 0111110 0111110));
[hear] (= (= 01110 01110) (= 011110 011110));
[hear] (= (= 01110 01110) (= 00 00));
[hear] (= (< 01111110 0110) (< 011110 0110));
[hear] (= (< 011110 010) (> 00 00));
[hear] (= (> 00 0111110) (= 01110 0110));
[hear] (= (> 0110 01110) (> 011110 0111110));
[hear] (= (> 0110 01111110) (> 010 01111110));
[hear] (not / = (> 0110 01110) (< 010 011110));
[hear] (not / = (= 011110 01110) (< 010 0110));
[hear] (not / = (= 0111110 011110) (< 0110 011110));
[hear] (not / = (> 011110 01111110) (= 01110 01110));
[hear] (not / = (= 01110 010) (> 011110 010));
[hear] (not /
= (< 01110 01111110) (< 01111110 0110));
[hear] (not / = (= 0110 0110) (> 0110 0111110));
[hear] (not /
= (= 0111110 0111110) (< 01111110 0110));
[hear] (not / = (= 01110 01110) (< 011110 01110));
[hear] (not / = (> 0111110 0110) (< 0111110 011110));
[hear] (define true 1);
[hear] (define false 0);
[hear] (= (true) (= 010 010));
[hear] (= (true) (= 00 00));
[hear] (= (true) (> 011111110 0111110));
[hear] (= (true) (= 0111110 0111110));
[hear] (= (true) (= 011110 011110));
[hear] (= (< 0111110 01111110) (true));
[hear] (= (= 0111110 0111110) (true));
[hear] (= (> 011111110 0111110) (true));
[hear] (= (= 0110 0110) (true));
[hear] (= (< 01110 01111110) (true));
[hear] (= (false) (< 0111110 00));
[hear] (= (false) (= 0110 01110));
[hear] (= (false) (< 01111110 0110));
[hear] (= (false) (> 010 0110));
[hear] (= (false) (> 0110 0111110));
[hear] (= (= 011110 01110) (false));
[hear] (= (= 00 010) (false));
[hear] (= (< 01111110 01110) (false));
[hear] (= (= 01110 00) (false));
[hear] (= (= 011110 01110) (false));
[hear] (= (true) (true));
[hear] (= (false) (false));
[hear] (not / = (true) (false));
[hear] (not / = (false) (true));
# MATH show mechanisms for branching
[hear] (intro if);
[hear] (= 28 / if (< 3 0) 24 28);
[hear] (= 27 / if (> 2 4) 29 27);
[hear] (= 29 / if (= 3 1) 20 29);
[hear] (= 21 / if (= 0 0) 21 26);
[hear] (= 29 / if (> 5 3) 29 23);
[hear] (= 26 / if (> 1 0) 26 22);
[hear] (= 21 / if (= 3 3) 21 27);
[hear] (= 23 / if (> 4 4) 25 23);
[hear] (define max /
? x /
? y /
if (> (x) (y)) (x) (y));
[hear] (define min /
? x /
? y /
if (< (x) (y)) (x) (y));
[hear] (= 0 / max 0 0);
[hear] (= 0 / min 0 0);
[hear] (= 1 / max 0 1);
[hear] (= 0 / min 0 1);
[hear] (= 2 / max 0 2);
[hear] (= 0 / min 0 2);
[hear] (= 1 / max 1 0);
[hear] (= 0 / min 1 0);
[hear] (= 1 / max 1 1);
[hear] (= 1 / min 1 1);
[hear] (= 2 / max 1 2);
[hear] (= 1 / min 1 2);
[hear] (= 2 / max 2 0);
[hear] (= 0 / min 2 0);
[hear] (= 2 / max 2 1);
[hear] (= 1 / min 2 1);
[hear] (= 2 / max 2 2);
[hear] (= 2 / min 2 2);
# need to be careful about whether 'if' is eager or lazy
# here we suggest that it is lazy
[hear] (define factorial /
? n /
if (< (n) 1) 1 /
* (n) /
factorial /
- (n) 1);
[hear] (= 1 / factorial 1);
[hear] (= 2 / factorial 2);
[hear] (= 6 / factorial 3);
[hear] (= 24 / factorial 4);
[hear] (= 120 / factorial 5);
# MATH introduce the AND logical operator
[hear] (intro and);
[hear] (define and
(? x /
? y /
if (x) (if (y) (true) (false)) (false)));
[hear] (and (= 0110 0110) (> 011110 0110));
[hear] (and (= 010 010) (> 01111110 011110));
[hear] (and (< 01110 011110) (= 0111110 0111110));
[hear] (and (= 01110 01110) (= 011110 011110));
[hear] (and (= 01110 01110) (= 00 00));
[hear] (and (< 0111110 011111110) (> 0111110 01110));
[hear] (and (> 0111110 011110) (> 010 00));
[hear] (and (> 01110 00) (= 01110 01110));
[hear] (and (< 01110 011110) (< 01110 01111110));
[hear] (and (> 0111110 011110) (> 0111110 011110));
[hear] (not / and (> 01111110 011110) (< 01110 010));
[hear] (not / and (> 01110 010) (> 01110 01110));
[hear] (not / and (= 00 00) (= 0111110 011110));
[hear] (not /
and (< 0110 011110) (> 011110 01111110));
[hear] (not / and (= 01110 01110) (= 01110 010));
[hear] (not /
and (> 010 0111110) (< 01110 01111110));
[hear] (not / and (< 01111110 0110) (= 0110 0110));
[hear] (not /
and (> 0110 0111110) (= 0111110 0111110));
[hear] (not / and (< 01111110 0110) (= 01110 01110));
[hear] (not / and (< 011110 01110) (> 0111110 0110));
[hear] (not / and (< 0111110 011110) (= 010 0110));
[hear] (not /
and (< 01111110 011110) (= 0111110 010));
[hear] (not / and (> 0110 01111110) (= 010 0111110));
[hear] (not / and (< 01111110 01110) (= 0110 01110));
[hear] (not / and (< 01111110 011110) (> 00 010));
[hear] (not / and (= 01110 0111110) (< 011110 010));
[hear] (not / and (= 011110 010) (< 011110 0110));
[hear] (not / and (< 01111110 01110) (= 01110 00));
[hear] (not /
and (< 011110 0110) (< 011110 01111110));
[hear] (not / and (> 011110 010) (< 0111110 0110));
[hear] (not / and (> 00 010) (> 011111110 0111110));
[hear] (not /
and (< 01110 011110) (> 01110 01111110));
[hear] (not / and (> 010 0110) (> 01111110 011110));
[hear] (not / and (< 00 010) (= 011110 0111110));
[hear] (and (< 011110 01111110) (< 0111110 011111110));
# MATH introduce the OR logical operator
[hear] (define or
(? x /
? y /
if (x) (true) (if (y) (true) (false))));
[hear] (intro or);
[hear] (or (= 0110 0110) (> 011110 0110));
[hear] (or (= 010 010) (> 01111110 011110));
[hear] (or (< 01110 011110) (= 0111110 0111110));
[hear] (or (= 01110 01110) (= 011110 011110));
[hear] (or (= 01110 01110) (= 00 00));
[hear] (or (< 0111110 011111110) (> 0111110 01110));
[hear] (or (> 0111110 011110) (> 010 00));
[hear] (or (> 01110 00) (= 01110 01110));
[hear] (or (< 01110 011110) (< 01110 01111110));
[hear] (or (> 0111110 011110) (> 0111110 011110));
[hear] (or (> 01111110 011110) (< 01110 010));
[hear] (or (> 01110 010) (> 01110 01110));
[hear] (or (= 00 00) (= 0111110 011110));
[hear] (or (< 0110 011110) (> 011110 01111110));
[hear] (or (= 01110 01110) (= 01110 010));
[hear] (or (> 010 0111110) (< 01110 01111110));
[hear] (or (< 01111110 0110) (= 0110 0110));
[hear] (or (> 0110 0111110) (= 0111110 0111110));
[hear] (or (< 01111110 0110) (= 01110 01110));
[hear] (or (< 011110 01110) (> 0111110 0110));
[hear] (not / or (< 0111110 011110) (= 010 0110));
[hear] (not /
or (< 01111110 011110) (= 0111110 010));
[hear] (not / or (> 0110 01111110) (= 010 0111110));
[hear] (not / or (< 01111110 01110) (= 0110 01110));
[hear] (not / or (< 01111110 011110) (> 00 010));
[hear] (not / or (= 01110 0111110) (< 011110 010));
[hear] (not / or (= 011110 010) (< 011110 0110));
[hear] (not / or (< 01111110 01110) (= 01110 00));
[hear] (or (< 011110 0110) (< 011110 01111110));
[hear] (or (> 011110 010) (< 0111110 0110));
[hear] (or (> 00 010) (> 011111110 0111110));
[hear] (or (< 01110 011110) (> 01110 01111110));
[hear] (or (> 010 0110) (> 01111110 011110));
[hear] (or (< 00 010) (= 011110 0111110));
[hear] (or (< 011110 01111110) (< 0111110 011111110));
[hear] (define >=
(? x /
? y /
or (> (x) (y)) (= (x) (y))));
[hear] (define <=
(? x /
? y /
or (< (x) (y)) (= (x) (y))));
[hear] (>= 0 0);
[hear] (<= 0 0);
[hear] (not / >= 0 1);
[hear] (<= 0 1);
[hear] (not / >= 0 2);
[hear] (<= 0 2);
[hear] (>= 1 0);
[hear] (not / <= 1 0);
[hear] (>= 1 1);
[hear] (<= 1 1);
[hear] (not / >= 1 2);
[hear] (<= 1 2);
[hear] (>= 2 0);
[hear] (not / <= 2 0);
[hear] (>= 2 1);
[hear] (not / <= 2 1);
[hear] (>= 2 2);
[hear] (<= 2 2);
# MATH illustrate pairs
[hear] (define cons (? x / ? y / ? f / f (x) (y)));
[hear] (define car
(? pair /
pair (? x / ? y / x)));
[hear] (define cdr
(? pair /
pair (? x / ? y / y)));
[hear] (assign x (cons 0 4) / = (car / x) 0);
[hear] (assign x (cons 0 4) / = (cdr / x) 4);
[hear] (assign x (cons 6 2) / = (car / x) 6);
[hear] (assign x (cons 6 2) / = (cdr / x) 2);
[hear] (assign x (cons 3 9) / = (car / x) 3);
[hear] (assign x (cons 3 9) / = (cdr / x) 9);
[hear] (assign x (cons 7 / cons 10 2) /
=