# Author: Paul Fitzpatrick, paulfitz@ai.mit.edu
# Copyright (c) 2004 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, then count down, then go through primes, etc.
# There is a bunch of syntax around the numbers, but that
# can just be treated as noise at this point - it doesn't matter.
# The key is to set up the structure of ';'-terminated sequences,
# and to introduce one simple representation of numbers.
# Symbols like intro and unary are encoded as binary numbers,
# which again can be treated as noise for now.
[hear] (intro / unary 0);
[hear] (intro / unary 1 0);
[hear] (intro / unary 1 1 0);
[hear] (intro / unary 1 1 1 0);
[hear] (intro / unary 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 0);
[hear] (intro / unary 1 1 1 0);
[hear] (intro / unary 1 1 0);
[hear] (intro / unary 1 0);
[hear] (intro / unary 0);
[hear] (intro / unary 0);
[hear] (intro / unary 1 0);
[hear] (intro / unary 1 1 0);
[hear] (intro / unary 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 0);
[hear] (intro / unary 1 0);
[hear] (intro / unary 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 0);
[hear] (intro / unary 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 0);
[hear] (intro / unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0);
# 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] (intro =);
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
# MATH now introduce other relational operators
# After this lesson, it should be clear what contexts
# < > and = are appropriate in.
[hear] (intro >);
[hear] (> (unary 1 1 1 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 0) (unary 1 0));
[hear] (> (unary 1 1 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 1 0) (unary 1 1 1 0));
[hear] (> (unary 1 1 0) (unary 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (> (unary 1 1 0) (unary 0));
[hear] (> (unary 1 1 0) (unary 0));
[hear] (> (unary 1 1 1 0) (unary 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 1 0) (unary 1 1 0));
[hear] (intro <);
[hear] (< (unary 1 1 0) (unary 1 1 1 1 1 0));
[hear] (< (unary 0) (unary 1 1 0));
[hear] (< (unary 0) (unary 1 1 1 1 1 0));
[hear] (< (unary 1 0) (unary 1 1 1 0));
[hear] (< (unary 0) (unary 1 1 1 0));
[hear] (< (unary 1 0) (unary 1 1 1 0));
[hear] (< (unary 1 1 0) (unary 1 1 1 1 1 1 0));
[hear] (< (unary 0) (unary 1 0));
[hear] (< (unary 0) (unary 1 1 1 1 1 1 0));
[hear] (< (unary 0) (unary 1 1 1 1 1 1 0));
[hear] (< (unary 1 0) (unary 1 1 1 1 0));
# drive the lesson home
[hear] (= (unary 0) (unary 0));
[hear] (< (unary 0) (unary 1 0));
[hear] (< (unary 0) (unary 1 1 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (= (unary 1 0) (unary 1 0));
[hear] (< (unary 1 0) (unary 1 1 0));
[hear] (> (unary 1 1 0) (unary 0));
[hear] (> (unary 1 1 0) (unary 1 0));
[hear] (= (unary 1 1 0) (unary 1 1 0));
[hear] (< (unary 1 0) (unary 1 1 1 1 1 0));
[hear] (< (unary 1 0) (unary 1 1 1 1 0));
[hear] (< (unary 0) (unary 1 0));
[hear] (> (unary 1 1 1 1 0) (unary 0));
[hear] (< (unary 1 1 0) (unary 1 1 1 0));
[hear] (> (unary 1 1 1 1 0) (unary 1 0));
[hear] (< (unary 0) (unary 1 1 1 1 1 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (< (unary 1 0) (unary 1 1 1 1 0));
[hear] (> (unary 1 1 0) (unary 0));
[hear] (< (unary 1 0) (unary 1 1 0));
# SYNTAX introduce tail notation
# I've recently added the / symbol to reduce the need
# for unnecessary levels of nesting and parentheses.
# This might be a little early to talk about it, since it
# is most valuable for complex expressions.
[hear] (= (unary 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 0) / unary 1 1 0);
[hear] (< (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (< (unary 1 1 0) / unary 1 1 1 1 0);
[hear] (> (unary 1 1 0) (unary 1 0));
[hear] (> (unary 1 1 0) / unary 1 0);
# MATH introduce the NOT logical operator
[hear] (intro not);
[hear] (= (unary 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not / < (unary 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not / > (unary 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 0) (unary 1 0));
[hear] (not / < (unary 1 0) (unary 1 0));
[hear] (not / > (unary 1 0) (unary 1 0));
[hear] (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not / < (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not / > (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (= (unary 0) (unary 0));
[hear] (not / < (unary 0) (unary 0));
[hear] (not / > (unary 0) (unary 0));
[hear] (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not / < (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not / > (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not / < (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not / > (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not / = (unary 0) (unary 1 0));
[hear] (< (unary 0) (unary 1 0));
[hear] (not / > (unary 0) (unary 1 0));
[hear] (not / = (unary 1 0) (unary 1 1 1 1 0));
[hear] (< (unary 1 0) (unary 1 1 1 1 0));
[hear] (not / > (unary 1 0) (unary 1 1 1 1 0));
[hear] (not / = (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (< (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (not / > (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (not / = (unary 1 1 1 0) (unary 1 1 1 1 0));
[hear] (< (unary 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not / > (unary 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not / = (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
[hear] (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
[hear] (not / > (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
[hear] (not / = (unary 0) (unary 1 1 1 0));
[hear] (< (unary 0) (unary 1 1 1 0));
[hear] (not / > (unary 0) (unary 1 1 1 0));
[hear] (not / = (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not / < (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not / = (unary 1 0) (unary 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (not / < (unary 1 0) (unary 0));
[hear] (not / = (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not / < (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not / = (unary 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not / < (unary 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not / = (unary 1 1 1 1 0) (unary 1 1 0));
[hear] (> (unary 1 1 1 1 0) (unary 1 1 0));
[hear] (not / < (unary 1 1 1 1 0) (unary 1 1 0));
[hear] (not / = (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not / < (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));
# MATH introduce the AND logical operator
[hear] (intro and);
[hear] (and (> (unary 1 1 1 0) (unary 1 0)) (< (unary 1 0) (unary 1 1 1 0)));
[hear] (and (= (unary 1 0) (unary 1 0)) (= (unary 1 0) (unary 1 0)));
[hear] (and (> (unary 1 1 1 1 1 0) (unary 1 1 0)) (= (unary 1 0) (unary 1 0)));
[hear] (and (> (unary 1 1 1 1 1 0) (unary 1 1 0))
(> (unary 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (and (> (unary 1 1 1 1 1 0) (unary 1 1 1 0)) (> (unary 1 1 1 0) (unary 1 0)));
[hear] (and (> (unary 1 1 1 0) (unary 1 0)) (< (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (and (> (unary 1 1 1 1 0) (unary 1 0))
(= (unary 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (and (< (unary 1 0) (unary 1 1 0)) (= (unary 1 1 0) (unary 1 1 0)));
[hear] (and (< (unary 1 1 0) (unary 1 1 1 1 1 0)) (< (unary 0) (unary 1 1 0)));
[hear] (and (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)) (= (unary 0) (unary 0)));
[hear] (not /
and (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0))
(= (unary 1 0) (unary 1 1 1 1 1 0)));
[hear] (not /
and (> (unary 1 1 1 1 0) (unary 1 1 0))
(= (unary 1 1 1 0) (unary 1 1 0)));
[hear] (not /
and (= (unary 1 1 1 0) (unary 1 1 1 0))
(> (unary 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (not /
and (< (unary 1 1 0) (unary 1 1 1 1 0))
(> (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (not /
and (= (unary 1 1 1 1 0) (unary 1 1 1 1 0))
(= (unary 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not / and (= (unary 1 1 1 0) (unary 1 1 0)) (< (unary 0) (unary 1 1 1 0)));
[hear] (not /
and (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))
(< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (not / and (< (unary 1 1 1 1 1 0) (unary 1 0)) (= (unary 1 0) (unary 1 0)));
[hear] (not / and (> (unary 0) (unary 1 1 0)) (< (unary 1 0) (unary 1 1 1 1 0)));
[hear] (not /
and (> (unary 1 1 1 1 0) (unary 1 1 1 1 1 0))
(> (unary 1 1 1 1 0) (unary 1 1 0)));
[hear] (not / and (< (unary 1 1 1 1 0) (unary 1 0)) (> (unary 1 0) (unary 1 1 0)));
[hear] (not /
and (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0))
(> (unary 0) (unary 1 1 0)));
[hear] (not /
and (= (unary 1 1 1 1 1 0) (unary 1 0))
(= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (not /
and (= (unary 1 1 1 1 1 0) (unary 1 1 1 0))
(< (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (not /
and (< (unary 1 1 0) (unary 0)) (= (unary 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (not /
and (= (unary 0) (unary 1 0)) (< (unary 1 1 1 1 1 1 0) (unary 1 1 0)));
[hear] (and (< (unary 0) (unary 1 1 1 0)) (= (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (not /
and (> (unary 1 1 1 1 0) (unary 1 1 1 1 0))
(< (unary 1 1 0) (unary 0)));
[hear] (not /
and (= (unary 1 1 0) (unary 1 1 1 0))
(> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (and (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
(< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (and (< (unary 1 0) (unary 1 1 1 1 0))
(< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (not /
and (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
(> (unary 1 1 1 0) (unary 1 0)));
[hear] (not /
and (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0))
(= (unary 1 1 0) (unary 1 1 1 0)));
[hear] (and (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0))
(< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not /
and (= (unary 0) (unary 1 1 1 0)) (= (unary 1 1 1 1 1 0) (unary 1 0)));
# MATH introduce the OR logical operator
[hear] (intro or);
[hear] (or (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)) (= (unary 1 0) (unary 1 0)));
[hear] (or (< (unary 1 1 0) (unary 1 1 1 1 0))
(= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)) (= (unary 1 0) (unary 1 0)));
[hear] (or (> (unary 1 1 0) (unary 1 0)) (> (unary 1 1 1 1 0) (unary 1 1 0)));
[hear] (or (> (unary 1 1 1 0) (unary 0)) (< (unary 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (or (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (< (unary 1 0) (unary 1 1 1 0)));
[hear] (or (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0))
(< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (or (< (unary 0) (unary 1 0)) (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (or (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0))
(< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (= (unary 1 0) (unary 1 0)) (< (unary 0) (unary 1 0)));
[hear] (or (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
(> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (or (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 1 1 0) (unary 0)));
[hear] (or (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0))
(> (unary 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (> (unary 1 1 1 1 0) (unary 1 1 1 0))
(> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (= (unary 1 0) (unary 1 0)) (= (unary 1 1 1 0) (unary 1 1 0)));
[hear] (or (< (unary 1 0) (unary 0)) (= (unary 1 1 0) (unary 1 1 0)));
[hear] (or (< (unary 1 1 1 0) (unary 1 0)) (= (unary 0) (unary 0)));
[hear] (or (> (unary 1 1 0) (unary 1 1 1 1 1 0))
(> (unary 1 1 1 1 0) (unary 1 1 0)));
[hear] (or (> (unary 1 1 1 0) (unary 1 1 1 1 1 0)) (= (unary 1 1 0) (unary 1 1 0)));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
(= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not / or (= (unary 1 0) (unary 1 1 1 0)) (= (unary 1 0) (unary 0)));
[hear] (not / or (> (unary 1 0) (unary 1 1 0)) (> (unary 1 0) (unary 1 1 1 1 0)));
[hear] (not /
or (= (unary 1 1 1 0) (unary 1 1 1 1 0))
(> (unary 1 0) (unary 1 1 1 1 0)));
[hear] (not / or (> (unary 0) (unary 1 1 1 1 0)) (= (unary 1 0) (unary 0)));
[hear] (not /
or (< (unary 1 1 1 1 0) (unary 1 0))
(< (unary 1 1 1 1 1 1 0) (unary 1 1 0)));
[hear] (not /
or (> (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
(= (unary 1 0) (unary 1 1 1 0)));
[hear] (or (> (unary 1 0) (unary 0)) (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (> (unary 1 0) (unary 0)) (= (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (> (unary 0) (unary 1 1 0)) (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (> (unary 1 1 0) (unary 1 1 1 1 0))
(< (unary 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (not /
or (= (unary 1 0) (unary 1 1 0)) (= (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (or (= (unary 1 1 1 0) (unary 1 1 1 1 0))
(> (unary 1 1 1 1 1 0) (unary 1 1 0)));
[hear] (not /
or (> (unary 1 0) (unary 1 1 1 1 1 1 0))
(< (unary 1 1 1 1 1 0) (unary 0)));
[hear] (or (< (unary 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 1 0) (unary 0)));
[hear] (or (= (unary 1 1 1 0) (unary 1 1 1 0)) (> (unary 1 1 0) (unary 1 1 1 0)));
# MATH use equality for truth values
[hear] (= (= (unary 1 1 1 1 0) (unary 1 1 1 1 0))
(< (unary 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (= (= (unary 1 0) (unary 1 0)) (< (unary 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (= (= (unary 1 0) (unary 1 0)) (> (unary 1 1 1 0) (unary 1 1 0)));
[hear] (= (< (unary 1 1 0) (unary 1 1 1 0))
(< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 0)));
[hear] (= (= (unary 1 1 1 1 0) (unary 1 1 1 1 0))
(< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (= (unary 1 1 1 0) (unary 0))
(> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (= (unary 1 1 1 1 0) (unary 1 1 1 1 1 0))
(> (unary 0) (unary 1 1 1 1 1 0)));
[hear] (= (= (unary 1 1 1 0) (unary 1 0)) (= (unary 1 1 0) (unary 1 1 1 0)));
[hear] (= (> (unary 1 1 1 0) (unary 1 1 1 1 0)) (> (unary 0) (unary 1 1 0)));
[hear] (= (= (unary 1 1 1 1 1 0) (unary 0)) (> (unary 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (not / = (> (unary 0) (unary 1 1 1 1 1 1 0)) (= (unary 1 0) (unary 1 0)));
[hear] (not / = (> (unary 1 1 0) (unary 1 1 1 0)) (= (unary 0) (unary 0)));
[hear] (not /
= (= (unary 1 1 1 1 0) (unary 1 1 1 1 1 0))
(< (unary 1 0) (unary 1 1 1 1 0)));
[hear] (not / = (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)) (= (unary 0) (unary 0)));
[hear] (not / = (= (unary 0) (unary 1 1 1 1 0)) (= (unary 1 1 0) (unary 1 1 0)));
[hear] (not /
= (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
(> (unary 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (not /
= (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)) (> (unary 0) (unary 1 1 0)));
[hear] (not /
= (= (unary 1 1 0) (unary 1 1 0)) (> (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (not / = (= (unary 1 0) (unary 1 0)) (< (unary 1 1 0) (unary 1 0)));
[hear] (not / = (= (unary 1 0) (unary 1 0)) (= (unary 1 0) (unary 1 1 1 1 0)));
[hear] (intro true);
[hear] (intro false);
[hear] (= (true) (< (unary 0) (unary 1 1 1 0)));
[hear] (= (true) (> (unary 1 1 1 1 0) (unary 1 0)));
[hear] (= (true) (> (unary 1 1 0) (unary 1 0)));
[hear] (= (true) (< (unary 1 0) (unary 1 1 1 1 0)));
[hear] (= (true) (< (unary 0) (unary 1 1 0)));
[hear] (= (= (unary 0) (unary 0)) (true));
[hear] (= (< (unary 1 1 1 0) (unary 1 1 1 1 0)) (true));
[hear] (= (> (unary 1 1 1 1 0) (unary 1 1 1 0)) (true));
[hear] (= (< (unary 0) (unary 1 0)) (true));
[hear] (= (> (unary 1 1 1 1 0) (unary 1 0)) (true));
[hear] (= (false) (> (unary 0) (unary 1 1 1 1 0)));
[hear] (= (false) (> (unary 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (= (false) (< (unary 1 1 1 0) (unary 0)));
[hear] (= (false) (< (unary 1 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (false) (> (unary 0) (unary 1 1 0)));
[hear] (= (< (unary 1 1 1 0) (unary 0)) (false));
[hear] (= (< (unary 1 1 1 1 1 1 0) (unary 1 0)) (false));
[hear] (= (> (unary 0) (unary 1 1 1 1 0)) (false));
[hear] (= (= (unary 1 0) (unary 1 1 1 0)) (false));
[hear] (= (> (unary 1 0) (unary 1 1 0)) (false));
[hear] (= (true) (true));
[hear] (= (false) (false));
[hear] (not / = (true) (false));
[hear] (not / = (false) (true));
# MATH introduce addition
[hear] (intro +);
[hear] (= (unary 1 1 1 0) / + (unary 1 1 1 0) (unary 0));
[hear] (= (unary 1 1 1 1 1 0) / + (unary 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 0) / + (unary 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 0) / + (unary 0) (unary 1 0));
[hear] (= (unary 1 1 1 1 1 1 0) / + (unary 1 1 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 0) / + (unary 1 1 0) (unary 0));
[hear] (= (unary 1 1 1 1 1 1 0) / + (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 1 0) / + (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 0) / + (unary 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 1 1 1 0) / + (unary 1 0) (unary 1 1 1 1 0));
# MATH introduce subtraction
[hear] (intro -);
[hear] (= (unary 1 1 1 0) / - (unary 1 1 1 1 0) (unary 1 0));
[hear] (= (unary 1 1 1 0) / - (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 0) / - (unary 1 0) (unary 1 0));
[hear] (= (unary 1 1 0) / - (unary 1 1 1 1 1 0) (unary 1 1 1 0));
[hear] (= (unary 0) / - (unary 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 0) / - (unary 1 0) (unary 0));
[hear] (= (unary 1 1 1 1 0) / - (unary 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 1 1 0) / - (unary 1 1 1 1 0) (unary 1 0));
[hear] (= (unary 1 1 1 1 0) / - (unary 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 0) / - (unary 1 0) (unary 0));
# MATH introduce multiplication
[hear] (intro *);
[hear] (= (unary 0) / * (unary 0) (unary 0));
[hear] (= (unary 0) / * (unary 0) (unary 1 0));
[hear] (= (unary 0) / * (unary 0) (unary 1 1 0));
[hear] (= (unary 0) / * (unary 0) (unary 1 1 1 0));
[hear] (= (unary 0) / * (unary 1 0) (unary 0));
[hear] (= (unary 1 0) / * (unary 1 0) (unary 1 0));
[hear] (= (unary 1 1 0) / * (unary 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 1 0) / * (unary 1 0) (unary 1 1 1 0));
[hear] (= (unary 0) / * (unary 1 1 0) (unary 0));
[hear] (= (unary 1 1 0) / * (unary 1 1 0) (unary 1 0));
[hear] (= (unary 1 1 1 1 0) / * (unary 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 1 1 1 1 0) / * (unary 1 1 0) (unary 1 1 1 0));
[hear] (= (unary 0) / * (unary 1 1 1 0) (unary 0));
[hear] (= (unary 1 1 1 0) / * (unary 1 1 1 0) (unary 1 0));
[hear] (= (unary 1 1 1 1 1 1 0) / * (unary 1 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 0) / * (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 1 0) / * (unary 1 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 0) / * (unary 1 0) (unary 1 1 0));
[hear] (= (unary 1 0) / * (unary 1 0) (unary 1 0));
[hear] (= (unary 1 1 0) / * (unary 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 1 0) / * (unary 1 0) (unary 1 1 1 0));
[hear] (= (unary 1 0) / * (unary 1 0) (unary 1 0));
[hear] (= (unary 1 1 1 0) / * (unary 1 0) (unary 1 1 1 0));
[hear] (= (unary 0) / * (unary 0) (unary 0));
[hear] (= (unary 1 1 0) / * (unary 1 0) (unary 1 1 0));
[hear] (= (unary 0) / * (unary 0) (unary 0));
# 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.
[hear] (= (unary 0) (.));
[hear] (= (unary 1 0) (:));
[hear] (= (unary 1 1 0) (:.));
[hear] (= (unary 1 1 1 0) (::));
[hear] (= (unary 1 1 1 1 0) (:..));
[hear] (= (unary 1 1 1 1 1 0) (:.:));
[hear] (= (unary 1 1 1 1 1 1 0) (::.));
[hear] (= (unary 1 1 1 1 1 1 1 0) (:::));
[hear] (= (unary 1 1 1 1 1 1 1 1 0) (:...));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 0) (:..:));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 0) (:.:.));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 0) (:.::));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 0) (::..));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (::.:));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (:::.));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (::::));
[hear] (= (::..) (unary 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (::..) (unary 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (::::) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (.) (unary 0));
[hear] (= (:.:.) (unary 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:::) (unary 1 1 1 1 1 1 1 0));
[hear] (= (:.:.) (unary 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:::.) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (:.::) (unary 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:..:) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (:.) (unary 1 1 0));
[hear] (= (:.::) (unary 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (+ (.) (::..))
(::..));
[hear] (= (+ (:.:.) (::))
(::.:));
[hear] (= (+ (.) (::::))
(::::));
[hear] (= (+ (:...) (:..))
(::..));
[hear] (= (+ (::..) (.))
(::..));
[hear] (= (+ (:..:) (::.:))
(:.::.));
[hear] (= (+ (:.:) (::.))
(:.::));
[hear] (= (+ (:.::) (:::))
(:..:.));
[hear] (= (* (:..:) (::::))
(:....:::));
[hear] (= (* (:.) (:...))
(:....));
[hear] (= (* (.) (.)) (.));
[hear] (= (* (:.) (::.:))
(::.:.));
[hear] (= (* (:) (:::)) (:::));
[hear] (= (* (:) (:.)) (:.));
[hear] (= (* (::) (:::))
(:.:.:));
[hear] (= (* (:.:.) (:..))
(:.:...));
# MATH demonstrate idea of leaving gaps in an expression
# and then filling them in afterwards
# the examples given leave a lot to be desired!
[hear] ((? x / = 10 / + 7 / x) 3);
[hear] ((? x / = 5 / + 2 / x) 3);
[hear] ((? x / = 20 / + 7 / x) 13);
[hear] ((? x / = 24 / + 13 / x) 11);
[hear] ((? x / = 19 / + 10 / x) 9);
[hear] ((? x / = 8 / + 0 / x) 8);
[hear] ((? x / = 17 / + 8 / x) 9);
[hear] ((? x / = 13 / + 7 / x) 6);
[hear] (((? x / ? y / = 1 / * (x) (y)) 1) 1);
[hear] (((? x / ? y / = 11 / * (x) (y)) 11) 1);
[hear] (((? x / ? y / = 22 / * (x) (y)) 2) 11);
[hear] (((? x / ? y / = 120 / * (x) (y)) 15) 8);
[hear] (((? x / ? y / = 50 / * (x) (y)) 5) 10);
[hear] (((? x / ? y / = 32 / * (x) (y)) 8) 4);
[hear] (((? x / ? y / = 5 / * (x) (y)) 1) 5);
[hear] (((? x / ? y / = 27 / * (x) (y)) 3) 9);
[hear] ((((? z /
? x /
? y /
= (z) /
* (x) (y))
60)
15)
4);
[hear] ((((? z / ? x / ? y / = (z) / * (x) (y)) 0)
5)
0);
[hear] ((((? z /
? x /
? y /
= (z) /
* (x) (y))
165)
15)
11);
[hear] ((((? z /
? x /
? y /
= (z) /
* (x) (y))
104)
13)
8);
[hear] ((((? z /
? x /
? y /
= (z) /
* (x) (y))
36)
6)
6);
[hear] ((((? z / ? x / ? y / = (z) / * (x) (y)) 2)
2)
1);
[hear] ((((? z /
? x /
? y /
= (z) /
* (x) (y))
165)
15)
11);
[hear] ((((? z /
? x /
? y /
= (z) /
* (x) (y))
70)
10)
7);
# MATH show some simple function calls
# and show a way to remember functions across statements
[hear] (= 49 /
(? square / square 7) (? x / * (x) (x)));
[hear] (= 49 /
(? square / square 7) (? x / * (x) (x)));
[hear] (= 81 /
(? square / square 9) (? x / * (x) (x)));
[hear] (= 16 /
(? square / square 4) (? x / * (x) (x)));
[hear] (= 81 /
(? square / square 9) (? x / * (x) (x)));
[hear] (= 9 /
(? square / square 3) (? x / * (x) (x)));
[hear] (= 1 /
(? square / square 1) (? x / * (x) (x)));
[hear] (= 1 /
(? square / square 1) (? x / * (x) (x)));
[hear] (define square / ? x / * (x) (x));
[hear] (= (square 9) 81);
[hear] (= (square 2) 4);
[hear] (= (square 8) 64);
[hear] (= (square 1) 1);
[hear] (define plusone / ? x / + (x) 1);
[hear] (= (plusone 3) 4);
[hear] (= (plusone 6) 7);
[hear] (= (plusone 3) 4);
[hear] (= (plusone 0) 1);
# MATH show mechanisms for branching
[hear] (intro if);
[hear] (= (if (false) 5 0) 0);
[hear] (= (if (true) 3 0) 3);
[hear] (= (if (false) 6 6) 6);
[hear] (= (if (true) 7 9) 7);
[hear] (= (if (false) 6 6) 6);
[hear] (= (if (true) 2 7) 2);
[hear] (= (if (true) 0 6) 0);
[hear] (= (if (true) 6 9) 6);
[hear] (= (if (true) 0 4) 0);
[hear] (= (if (false) 9 8) 8);
[hear] (= (if (true) 4 6) 4);
[hear] (= (if (false) 1 3) 3);
[hear] (= (if (true) 7 3) 7);
[hear] (= (if (false) 4 9) 9);
[hear] (= (if (false) 2 1) 1);
[hear] (= (if (true) 1 0) 1);
# MATH some pure lambda calculus definitions - optional
# these definitions are not quite what we want
# since thinking of everything as a function requires headscratching
# it would be better to use these as a parallel means of evaluation
# ... for expressions
[hear] (define pure-if /
? x /
? y /
? z /
x (y) (z));
[hear] (define pure-true / ? y / ? z / y);
[hear] (define pure-false / ? y / ? z / z);
[hear] (define pure-cons /
? x /
? y /
? z /
pure-if (z) (x) (y));
[hear] (define pure-car / ? x / x (pure-true));
[hear] (define pure-cdr / ? x / x (pure-false));
[hear] (define zero / ? f / ? x / x);
[hear] (define one / ? f / ? x / f (x));
[hear] (define two / ? f / ? x / f (f (x)));
[hear] (define succ /
? n /
? f /
? x /
f ((n (f)) (x)));
[hear] (define add / ? a / ? b / (a (succ)) (b));
[hear] (define mult /
? a /
? b /
(a (add / b)) (zero));
[hear] (define pred /
? n /
pure-cdr /
(n (? p /
pure-cons
(succ /
pure-car /
p)
(pure-car /
p)))
(pure-cons (zero) (zero)));
[hear] (define is-zero /
? n /
(n (? dummy / pure-false) (pure-true)));
[hear] (define fixed-point /
? f /
(? x / f (x (x))) (? x / f (x (x))));
# .. but for rest of message will assume that define does fixed-point for us
# now build a link between numbers and church number functions
[hear] (define unchurch /
? c /
c (? x / + (x) 1) 0);
[hear] (= 0 (unchurch / zero));
[hear] (= 1 (unchurch / one));
[hear] (= 2 (unchurch / two));
[hear] (define church /
? x /
if (= 0 (x))
(zero)
(succ /
church /
- (x) 1));
# MATH show an example of recursive evaluation
# skipping over a lot of definitions and desugarings
[hear] (define easy-factorial /
? f /
? x /
if (> (x) 0) (* (x) / f (f) (- (x) 1)) 1);
[hear] (define factorial /
? x /
if (> (x) 0)
(* (x) /
factorial /
- (x) 1)
1);
[hear] (= (easy-factorial (easy-factorial) 0) 1);
[hear] (= (easy-factorial (easy-factorial) 1) 1);
[hear] (= (easy-factorial (easy-factorial) 2) 2);
[hear] (= (easy-factorial (easy-factorial) 3) 6);
[hear] (= (easy-factorial (easy-factorial) 4) 24);
[hear] (= (easy-factorial (easy-factorial) 5) 120);
[hear] (= (factorial 0) 1);
[hear] (= (factorial 1) 1);
[hear] (= (factorial 2) 2);
[hear] (= (factorial 3) 6);
[hear] (= (factorial 4) 24);
[hear] (= (factorial 5) 120);
# MATH introduce universal quantifier
# really need to link with sets for true correctness
# and the examples here are REALLY sparse, need much more
[hear] (intro forall);
[hear] (< 5 (+ 5 1));
[hear] (< 4 (+ 4 1));
[hear] (< 3 (+ 3 1));
[hear] (< 2 (+ 2 1));
[hear] (< 1 (+ 1 1));
[hear] (< 0 (+ 0 1));
[hear] (forall (? x / < (x) (+ (x) 1)));
[hear] (< 5 (* 5 2));
[hear] (< 4 (* 4 2));
[hear] (< 3 (* 3 2));
[hear] (< 2 (* 2 2));
[hear] (< 1 (* 1 2));
[hear] (not / < 0 (* 0 2));
[hear] (not / forall (? x / < (x) (* (x) 2)));
# MATH introduce existential quantifier
# really need to link with sets for true correctness
# and the examples here are REALLY sparse, need much more
[hear] (not / = 5 (* 2 2));
[hear] (= 4 (* 2 2));
[hear] (not / = 3 (* 2 2));
[hear] (not / = 2 (* 2 2));
[hear] (not / = 1 (* 2 2));
[hear] (not / = 0 (* 2 2));
[hear] (intro exists);
[hear] (exists (? x / = (x) (* 2 2)));
[hear] (not / = 5 (+ 5 2));
[hear] (not / = 4 (+ 4 2));
[hear] (not / = 3 (+ 3 2));
[hear] (not / = 2 (+ 2 2));
[hear] (not / = 1 (+ 1 2));
[hear] (not / = 0 (+ 0 2));
[hear] (not (exists (? x / = (x) (+ (x) 2))));
# MATH introduce logical implication
[hear] (intro =>);
[hear] (define => /
? x /
? y /
not /
and (x) (not / y));
[hear] (=> (true) (true));
[hear] (not / => (true) (false));
[hear] (=> (false) (true));
[hear] (=> (false) (false));
[hear] (forall
(? x /
forall
(? y /
=> (=> (x) (y)) (=> (not / y) (not / x)))));
# MATH illustrate lists and some list operators
# to make list describable as a function, need to preceed lists
# ... with an argument count
# lists will be written as [1 2 1] = (list 3 1 2 1) after this lesson
# it would be nice to include such syntactic sugar in the message but that
# ... is a fight for another day
# finally, lists keep an explicit record of their length
# this is to avoid the need for using a special 'nil' symbol
# ... which cannot itself be placed in the list.
#
# missing - intro to cons, car, cdr
# used to be pure-cons pure-car pure-cdr but changed for better interface to scheme
# also should introduce number? check function
#
[hear] (define list-helper /
? n /
? ret /
if (> (n) 1)
(? x /
list-helper
(- (n) 1)
(? y /
? z /
ret (+ 1 (y)) (cons (x) (z))))
(? x /
ret 1 (x)));
[hear] (define list /
? n /
if (= (n) 0)
(cons 0 0)
(list-helper (n) (? y / ? z / cons (y) (z))));
[hear] (define head /
? lst /
if (= (car / lst) 0)
(undefined)
(if (= (car / lst) 1)
(cdr /
lst)
(car /
cdr /
lst)));
[hear] (define tail /
? lst /
if (= (car / lst) 0)
(undefined)
(if (= (car / lst) 1)
(cons 0 0)
(cons (- (car / lst) 1) (cdr / cdr / lst))));
[hear] (define list-length / ? lst / car / lst);
[hear] (define list-ref /
? lst /
? n /
if (= (list-ref / lst) 0)
(undefined)
(if (= (n) 0)
(head /
lst)
(list-ref (tail / lst) (- (n) 1))));
[hear] (define prepend /
? x /
? lst /
if (= (list-length / lst) 0)
(cons 1 (x))
(cons (+ (list-length / lst) 1)
(cons (x) (cdr / lst))));
[hear] (define list= /
? x /
? y /
if (= (list-length / x) (list-length / y))
(if (> (list-length / x) 0)
(and (= (head / x) (head / y))
(list= (tail / x) (tail / y)))
(true))
(false));
[hear] (= (list-length / (list 4) 4 8 5 0) 4);
[hear] (= (list-length / (list 5) 3 1 4 6 5) 5);
[hear] (= (list-length / (list 6) 5 0 3 4 7 8) 6);
[hear] (= (list-length / (list 7) 0 8 7 4 9 1 5) 7);
[hear] (= (list-length / (list 3) 0 3 6) 3);
[hear] (= (head / (list 5) 9 9 12 16 0) 9);
[hear] (list= (tail /
(list 5) 9 9 12 16 0)
((list 4) 9 12 16 0));
[hear] (= (head / (list 2) 1 16) 1);
[hear] (list= (tail / (list 2) 1 16) ((list 1) 16));
[hear] (= (head / (list 8) 17 11 7 14 0 12 13 11) 17);
[hear] (list= (tail /
(list 8) 17 11 7 14 0 12 13 11)
((list 7) 11 7 14 0 12 13 11));
[hear] (= (head / (list 8) 15 17 8 6 10 18 19 14) 15);
[hear] (list= (tail /
(list 8) 15 17 8 6 10 18 19 14)
((list 7) 17 8 6 10 18 19 14));
[hear] (= (head / (list 4) 4 7 12 12) 4);
[hear] (list= (tail /
(list 4) 4 7 12 12)
((list 3) 7 12 12));
[hear] (= (head / (list 4) 6 10 6 8) 6);
[hear] (list= (tail /
(list 4) 6 10 6 8)
((list 3) 10 6 8));
[hear] (= (head / (list 2) 9 4) 9);
[hear] (list= (tail / (list 2) 9 4) ((list 1) 4));
[hear] (= (head / (list 9) 7 4 19 17 14 10 5 7 5) 7);
[hear] (list= (tail /
(list 9) 7 4 19 17 14 10 5 7 5)
((list 8) 4 19 17 14 10 5 7 5));
[hear] (= (head / (list 1) 11) 11);
[hear] (list= (tail / (list 1) 11) ((list 0)));
[hear] (= (head / (list 1) 1) 1);
[hear] (list= (tail / (list 1) 1) ((list 0)));
[hear] (= (list-ref ((list 3) 16 2 19) 1) 2);
[hear] (= (list-ref ((list 9) 19 15 15 13 17 6 10 17 14) 0)
19);
[hear] (= (list-ref ((list 5) 13 13 10 16 7) 2) 10);
[hear] (= (list-ref ((list 7) 6 17 19 3 0 14 15) 1) 17);
[hear] (= (list-ref ((list 10) 17 3 1 4 15 0 3 10 13 9) 2)
1);
[hear] (= (list-ref ((list 4) 8 0 6 18) 0) 8);
[hear] (= (list-ref
((list 10) 13 19 19 15 13 11 15 11 3 7)
6)
15);
[hear] (= (list-ref ((list 5) 10 13 7 10 5) 1) 13);
[hear] (= (list-ref ((list 2) 5 2) 1) 2);
[hear] (= (list-ref ((list 1) 14) 0) 14);
[hear] (list= ((list 0)) ((list 0)));
[hear] (list= ((list 1) 7) ((list 1) 7));
[hear] (list= ((list 2) 9 4) ((list 2) 9 4));
[hear] (list= ((list 3) 1 2 13) ((list 3) 1 2 13));
[hear] (list= ((list 4) 17 17 9 6) ((list 4) 17 17 9 6));
# this next batch of examples are a bit misleading, should streamline
[hear] (not / list= ((list 0)) ((list 1) 4));
[hear] (not / list= ((list 0)) ((list 1) 3));
[hear] (not / list= ((list 1) 7) ((list 2) 4 7));
[hear] (not / list= ((list 1) 7) ((list 2) 7 0));
[hear] (not /
list= ((list 2) 17 10) ((list 3) 1 17 10));
[hear] (not /
list= ((list 2) 17 10) ((list 3) 17 10 3));
[hear] (not /
list= ((list 3) 12 11 3) ((list 4) 5 12 11 3));
[hear] (not /
list= ((list 3) 12 11 3) ((list 4) 12 11 3 1));
[hear] (not /
list= ((list 4) 8 11 3 17)
((list 5) 1 8 11 3 17));
[hear] (not /
list= ((list 4) 8 11 3 17)
((list 5) 8 11 3 17 3));
# some helpful functions
[hear] (list= (prepend 12 ((list 0))) ((list 1) 12));
[hear] (list= (prepend 5 ((list 1) 15)) ((list 2) 5 15));
[hear] (list= (prepend 16 ((list 2) 13 17))
((list 3) 16 13 17));
[hear] (list= (prepend 13 ((list 3) 12 4 11))
((list 4) 13 12 4 11));
[hear] (list= (prepend 12 ((list 4) 7 16 4 18))
((list 5) 12 7 16 4 18));
[hear] (list= (prepend 6 ((list 5) 15 19 17 17 6))
((list 6) 6 15 19 17 17 6));
[hear] (list= (prepend 12 ((list 6) 18 3 18 11 7 9))
((list 7) 12 18 3 18 11 7 9));
[hear] (list= (prepend 15 ((list 7) 19 14 13 16 8 1 10))
((list 8) 15 19 14 13 16 8 1 10));
[hear] (define pair /
? x /
? y /
(list 2) (x) (y));
[hear] (define first / ? lst / head / lst);
[hear] (define second /
? lst /
head /
tail /
lst);
[hear] (list= (pair 3 8) ((list 2) 3 8));
[hear] (= (first / pair 3 8) 3);
[hear] (= (second / pair 3 8) 8);
[hear] (list= (pair 7 4) ((list 2) 7 4));
[hear] (= (first / pair 7 4) 7);
[hear] (= (second / pair 7 4) 4);
[hear] (list= (pair 9 7) ((list 2) 9 7));
[hear] (= (first / pair 9 7) 9);
[hear] (= (second / pair 9 7) 7);
[hear] (define list-find-helper /
? lst /
? key /
? fail /
? idx /
if (= (list-length / lst) 0)
(fail 0)
(if (= (head / lst) (key))
(idx)
(list-find-helper
(tail /
lst)
(key)
(fail)
(+ (idx) 1))));
[hear] (define list-find /
? lst /
? key /
? fail /
list-find-helper (lst) (key) (fail) 0);
[hear] (define example-fail / ? x 100);
[hear] (= (list-find ((list 5) 5 4 2 1 0) 4 (example-fail))
1);
[hear] (= (list-find ((list 1) 5) 5 (example-fail)) 0);
[hear] (= (list-find
((list 5) 5 4 3 17 8)
4
(example-fail))
1);
[hear] (= (list-find ((list 4) 10 3 3 2) 10 (example-fail))
0);
[hear] (= (list-find
((list 7) 18 8 12 5 13 13 0)
13
(example-fail))
4);
[hear] (= (list-find
((list 6) 0 10 14 15 3 17)
15
(example-fail))
3);
[hear] (= (list-find
((list 9) 15 10 16 0 16 2 16 8 9)
10
(example-fail))
1);
[hear] (= (list-find ((list 3) 10 18 14) 18 (example-fail))
1);
[hear] (= (list-find ((list 2) 13 13) 13 (example-fail))
0);
[hear] (= (list-find
((list 7) 13 19 13 19 9 19 1)
13
(example-fail))
0);
[hear] (= (list-find ((list 4) 1 7 16 15) 6 (example-fail))
100);
[hear] (= (list-find
((list 6) 5 10 13 7 12 19)
8
(example-fail))
100);
[hear] (= (list-find
((list 8) 19 7 13 1 11 12 8 2)
16
(example-fail))
100);
# HACK describe changes to the implicit interpreter to allow new special forms
[hear] (define base-translate / translate);
[hear] (define translate /
? x /
if (= (x) 10) 15 (base-translate / x));
[hear] (= 10 15);
[hear] (= (+ 10 15) 30);
[hear] (define translate / base-translate);
[hear] (not / = 10 15);
[hear] (= (+ 10 15) 25);
# now can create a special form for lists
[hear] (define translate /
? x /
if (number? /
x)
(base-translate /
x)
(if (= (head / x) vector)
(translate /
prepend
((list 2) list (list-length / tail / x))
(tail /
x))
(base-translate /
x)));
[hear] (= (vector 1 2 3) ((list 3) 1 2 3));
# now to desugar let expressions
[hear] (define translate-with-vector / translate);
[hear] (define translate-let-form /
? x /
? body /
if (= (list-length / x) 0)
(translate /
body)
(translate-let-form
(tail /
x)
(vector
(vector ? (head / head / x) (body))
(head /
tail /
head /
x))));
[hear] (define translate /
? x /
if (number? /
x)
(translate-with-vector /
x)
(if (= (head / x) let)
(translate-let-form
(head /
tail /
x)
(head /
tail /
tail /
x))
(translate-with-vector /
x)));
[hear] (let ((x 20)) (= (x) 20));
[hear] (let ((x 50) (y 20)) (= (- (x) (y)) 30));
# the is-list function is now on dubious ground
# this stuff will be replaced with typing ASAP
[hear] (define is-list /
? x /
not /
number? /
x);
[hear] (is-list / (list 2) 1 3);
[hear] (is-list / (list 0));
[hear] (not / is-list 23);
[hear] (is-list /
(list 3) ((list 2) 2 3) 1 (? x / + (x) 10));
# MATH introduce sugar for let
# if would be good to introduce desugarings more rigorously, but for now...
# ... just a very vague sketch
[hear] (intro let);
[hear] (= (let ((x 10)) (+ (x) 5))
((? x / + (x) 5) 10));
[hear] (= (let ((x 10) (y 5)) (+ (x) (y)))
(((? x / ? y / + (x) (y)) 10) 5));
# MATH build up functions of several variables
[hear] (= ((? x / ? y / - (x) (y)) 3 3) 0);
[hear] (= ((? x / ? y / - (x) (y)) 8 7) 1);
[hear] (= ((? x / ? y / - (x) (y)) 13 9) 4);
[hear] (= ((? x / ? y / - (x) (y)) 15 9) 6);
[hear] (= ((? x / ? y / - (x) (y)) 8 5) 3);
[hear] (define last /
? x /
list-ref (x) (- (list-length / x) 1));
[hear] (define except-last /
? x /
if (> (list-length / x) 1)
(prepend
(head /
x)
(except-last /
tail /
x))
(vector));
# test last and except-last
[hear] (= 15 (last / vector 4 5 15));
[hear] (list= (vector 4 5)
(except-last /
vector 4 5 15));
[hear] (intro lambda);
[hear] (define prev-translate / translate);
[hear] (define translate /
let ((prev (prev-translate)))
(? x /
if (number? /
x)
(prev /
x)
(if (= (head / x) lambda)
(let ((formals (head / tail / x))
(body (head / tail / tail / x)))
(if (> (list-length / formals) 0)
(translate
(vector
lambda
(except-last /
formals)
(vector ? (last / formals) (body))))
(translate (body))))
(prev /
x))));
# test lambda
[hear] (= (? x / - (x) 5) (lambda (x) (- (x) 5)));
[hear] (= (? x /
? y /
- (x) (y))
(lambda (x y) (- (x) (y))));
[hear] (= ((lambda (x y) (- (x) (y))) 9 1) 8);
[hear] (= ((lambda (x y) (- (x) (y))) 15 7) 8);
[hear] (= ((lambda (x y) (- (x) (y))) 6 0) 6);
[hear] (= ((lambda (x y) (- (x) (y))) 11 8) 3);
[hear] (= ((lambda (x y) (- (x) (y))) 6 6) 0);
[hear] (define apply /
lambda (x y)
(if (list= (y) (vector))
(x)
(apply ((x) (head / y)) (tail / y))));
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 8 1))
7);
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 11 5))
6);
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 8 4))
4);
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 13 5))
8);
[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 9 4))
5);
# MATH show map function for applying a function across the elements of a list
[hear] (define map /
lambda (p lst)
(if (> (list-length / lst) 0)
(prepend
(p (head / lst))
(map (p) (tail / lst)))
(vector)));
[hear] (= (map (? x / * (x) 2) (vector 7 8 9))
(vector 14 16 18));
[hear] (= (map (? x / * (x) 2) (vector 19 7 13 10))
(vector 38 14 26 20));
[hear] (= (map (? x / * (x) 2) (vector 4 10 7 1 2))
(vector 8 20 14 2 4));
[hear] (= (map (? x / * (x) 2) (vector 3 18 16 7 9 13))
(vector 6 36 32 14 18 26));
[hear] (= (map (? x 42) (vector 5 16 15))
(vector 42 42 42));
[hear] (= (map (? x 42) (vector 13 9 7 14))
(vector 42 42 42 42));
[hear] (= (map (? x 42) (vector 1 16 3 19 15))
(vector 42 42 42 42 42));
[hear] (= (map (? x 42) (vector 15 5 2 12 16 14))
(vector 42 42 42 42 42 42));
[hear] (define crunch /
lambda (p lst)
(if (>= (list-length / lst) 2)
(p (head / lst) (crunch (p) (tail / lst)))
(if (= (list-length / lst) 1)
(head /
lst)
(undefined))));
[hear] (= (crunch (+) (vector 1 8 18)) 27);
[hear] (= (crunch (+) (vector 3 11 0 5)) 19);
[hear] (= (crunch (+) (vector 7 15 6 11 9)) 48);
[hear] (= (crunch (+) (vector 18 14 19 4 5 17)) 77);
# MATH introduce mutable objects, and side-effects
[hear] (intro make-cell);
[hear] (intro set!);
[hear] (intro get!);
[hear] (define demo-mut1 / make-cell 0);
[hear] (set! (demo-mut1) 15);
[hear] (= (get! / demo-mut1) 15);
[hear] (set! (demo-mut1) 5);
[hear] (set! (demo-mut1) 7);
[hear] (= (get! / demo-mut1) 7);
[hear] (define demo-mut2 / make-cell 11);
[hear] (= (get! / demo-mut2) 11);
[hear] (set! (demo-mut2) 22);
[hear] (= (get! / demo-mut2) 22);
[hear] (= (get! / demo-mut1) 7);
[hear] (= (+ (get! / demo-mut1) (get! / demo-mut2))
29);
[hear] (if (= (get! / demo-mut1) 7)
(set! (demo-mut1) 88)
(set! (demo-mut1) 99));
[hear] (= (get! / demo-mut1) 88);
[hear] (if (= (get! / demo-mut1) 7)
(set! (demo-mut1) 88)
(set! (demo-mut1) 99));
[hear] (= (get! / demo-mut1) 99);
# MATH show how to execute a sequence of instructions
[hear] (intro begin);
[hear] (define prev-translate / translate);
[hear] (define reverse /
? x /
if (>= (list-length / x) 1)
(prepend
(last /
x)
(reverse /
except-last /
x))
(x));
# test reverse
[hear] (list= (vector 1 2 3) (reverse / vector 3 2 1));
[hear] (define translate /
let ((prev (prev-translate)))
(? x /
if (number? /
x)
(prev /
x)
(if (= (head / x) begin)
(translate
(vector
(vector ? x (vector head (vector x)))
(prepend vector (reverse / tail / x))))
(prev /
x))));
[hear] (= (begin 1 7 2 4) 4);
[hear] (= (begin
(set! (demo-mut1) 88)
(set! (demo-mut1) 6)
(get! /
demo-mut1))
6);
[hear] (= (begin
(set! (demo-mut2) 88)
(set! (demo-mut1) 6)
(get! /
demo-mut2))
88);
[hear] (= (begin
(set! (demo-mut1) 88)
(set! (demo-mut1) 6)
(get! /
demo-mut1)
4)
4);
# MATH introduce environment / hashmap structure
# this section needs a LOT more examples :-
# note that at the time of writing (h 1 2) is same as ((h) 1 2)
[hear] (define hash-add /
lambda (h x y z) (if (= (z) (x)) (y) (h (z))));
[hear] (define hash-ref / lambda (h x) (h (x)));
[hear] (define hash-null / ? x / undefined);
[hear] (define test-hash /
hash-add (hash-add (hash-null) 3 2) 4 9);
[hear] (= (hash-ref (test-hash) 4) 9);
[hear] (= (hash-ref (test-hash) 3) 2);
[hear] (= (hash-ref (test-hash) 8) (undefined));
[hear] (= (hash-ref (test-hash) 15) (undefined));
[hear] (= (hash-ref (hash-add (test-hash) 15 33) 15) 33);
[hear] (= (hash-ref (test-hash) 15) (undefined));
[hear] (define make-hash /
? x /
if (list= (x) (vector))
(hash-null)
(hash-add
(make-hash (tail / x))
(first /
head /
x)
(second /
head /
x)));
[hear] (= (hash-ref
(make-hash /
vector (pair 3 10) (pair 2 20) (pair 1 30))
3)
10);
[hear] (= (hash-ref
(make-hash /
vector (pair 3 10) (pair 2 20) (pair 1 30))
1)
30);
# OBJECT introduce simple mutable structures
[hear] (define mutable-struct /
? lst /
let ((data (map (? x / make-cell 0) (lst))))
(? key /
list-ref (data) (list-find (lst) (key) (? x 0))));
[hear] (define test-struct1 /
mutable-struct /
vector item1 item2 item3);
[hear] (set! (test-struct1 item1) 15);
[hear] (= (get! / test-struct1 item1) 15);
# OBJECT introduce method handler wrappers
[hear] (define add-method /
lambda (object name method)
(hash-add
(object)
(name)
(? dummy /
method /
object)));
[hear] (define call / ? x / x 0);
[hear] (define test-struct2 /
mutable-struct /
vector x y);
[hear] (set! (test-struct2 x) 10);
[hear] (set! (test-struct2 y) 20);
[hear] (= (get! / test-struct2 x) 10);
[hear] (= (get! / test-struct2 y) 20);
[hear] (define test-struct3 /
add-method
(test-struct2)
sum
(? self /
+ (get! / self x) (get! / self y)));
[hear] (= (get! / test-struct3 x) 10);
[hear] (= (get! / test-struct3 y) 20);
[hear] (= (call / test-struct3 sum) 30);
[hear] (set! (test-struct3 y) 10);
[hear] (= (call / test-struct3 sum) 20);
[hear] (set! (test-struct2 y) 5);
[hear] (= (call / test-struct3 sum) 15);
# TURING introduce turing machine model
# just for fun!
[hear] (define safe-tail /
? x /
if (> (list-length / x) 0)
(if (> (list-length / x) 1)
(tail /
x)
(vector /
false))
(? vector /
false));
[hear] (define safe-head /
? x /
if (> (list-length / x) 0)
(head /
x)
(false));
[hear] (define tape-read /
? tape /
let ((x (second / tape)))
(if (> (list-length / x) 0)
(head /
x)
(false)));
[hear] (define tape-transition /
lambda (tape shift value)
(if (= (shift) 1)
(pair (prepend (value) (first / tape))
(safe-tail /
second /
tape))
(if (= (shift) 0)
(pair (safe-tail /
first /
tape)
(prepend
(safe-head /
first /
tape)
(prepend (value) (safe-tail / second / tape))))
(pair (first /
tape)
(prepend (value) (safe-tail / second / tape))))));
[hear] (define turing /
lambda (machine current last tape)
(if (= (current) (last))
(tape)
(let ((next (machine (current) (tape-read / tape))))
(turing
(machine)
(list-ref (next) 0)
(last)
(tape-transition
(tape)
(list-ref (next) 1)
(list-ref (next) 2))))));
[hear] (define make-tape /
? x /
pair (vector) (x));
[hear] (define remove-trail /
? x /
? lst /
if (> (list-length / lst) 0)
(if (= (last / lst) (x))
(remove-trail (x) (except-last / lst))
(lst))
(lst));
[hear] (define extract-tape /
? x /
remove-trail (false) (second / x));
[hear] (define tm-binary-increment /
make-hash /
vector
(pair right
(make-hash /
vector
(pair 0 (vector right 1 0))
(pair 1 (vector right 1 1))
(pair (false) (vector inc 0 (false)))))
(pair inc
(make-hash /
vector
(pair 0 (vector noinc 0 1))
(pair 1 (vector inc 0 0))
(pair (false) (vector halt 2 1))))
(pair noinc
(make-hash /
vector
(pair 0 (vector noinc 0 0))
(pair 1 (vector noinc 0 1))
(pair (false) (vector halt 1 (false)))))
(pair halt (make-hash / vector)));
[hear] (= (extract-tape /
turing
(tm-binary-increment)
right
halt
(make-tape /
vector 1 0 0 1))
(vector 1 0 1 0));
[hear] (= (extract-tape /
turing
(tm-binary-increment)
right
halt
(make-tape /
vector 1 1 1))
(vector 1 0 0 0));
[hear] (= (extract-tape /
turing
(tm-binary-increment)
right
halt
(make-tape /
vector 1 1 1 0 0 0 1 1 1))
(vector 1 1 1 0 0 1 0 0 0));
# MATH introduce sets and set membership
[hear] (intro element);
[hear] (define element /
? x /
? lst /
not /
= (list-find (lst) (x) (? y / false)) (false));
[hear] (element 8 (vector 8 6 4 1 9));
[hear] (element 9 (vector 8 6 4 1 9));
[hear] (element 1 (vector 8 6 4 1 9));
[hear] (element 6 (vector 8 6 4 1 0 7));
[hear] (element 8 (vector 8 6 4 1 0 7));
[hear] (element 4 (vector 8 6 4 1 0 7));
[hear] (element 7 (vector 8 1 0 7 9));
[hear] (element 7 (vector 8 1 0 7 9));
[hear] (element 0 (vector 8 1 0 7 9));
[hear] (element 8 (vector 8 0 7 9 5));
[hear] (element 8 (vector 8 0 7 9 5));
[hear] (element 9 (vector 8 0 7 9 5));
[hear] (element 8 (vector 8 6 1 3 9));
[hear] (element 3 (vector 8 6 1 3 9));
[hear] (element 1 (vector 8 6 1 3 9));
[hear] (not / element 6 (vector 7 2 5));
[hear] (not / element 6 (vector 4 7 2 5));
[hear] (not / element 6 (vector 3 0 5));
[hear] (not / element 8 (vector 4 0 3 7));
[hear] (not / element 1 (vector 0 3 9));
# rules for set equality
[hear] (define set-subset /
? x /
? y /
if (> (list-length / x) 0)
(and (element (head / x) (y))
(set-subset (tail / x) (y)))
(true));
[hear] (define set= /
? x /
? y /
and (set-subset (x) (y)) (set-subset (y) (x)));
[hear] (set= (vector 1 5 9) (vector 5 1 9));
[hear] (set= (vector 1 5 9) (vector 9 1 5));
[hear] (not / set= (vector 1 5 9) (vector 1 5));
# let's go leave ourselves wide open to Russell's paradox
# ... by using characteristic functions
# ... since it doesn't really matter for communication purposes
# ... and so far this is just used / tested with sets of integers really
[hear] (element 5 (all (? x / = (+ (x) 10) 15)));
[hear] (element 3 (all (? x / = (* (x) 3) (+ (x) 6))));
[hear] (define empty-set / vector);
[hear] (element 0 (natural-set));
[hear] (forall
(? x /
=> (element (x) (natural-set))
(element (+ (x) 1) (natural-set))));
[hear] (element 1 (natural-set));
[hear] (element 2 (natural-set));
[hear] (element 3 (natural-set));
[hear] (element 4 (natural-set));
[hear] (element 5 (natural-set));
[hear] (element 6 (natural-set));
[hear] (element 7 (natural-set));
[hear] (element 8 (natural-set));
[hear] (element 9 (natural-set));
[hear] (not / element (true) (natural-set));
[hear] (not / element (false) (natural-set));
[hear] (define boolean-set / vector (true) (false));
[hear] (element (true) (boolean-set));
[hear] (element (false) (boolean-set));
[hear] (not / element 0 (boolean-set));
[hear] (define even-natural-set /
all /
? x /
exists /
? y /
and (element (y) (natural-set))
(= (* 2 (y)) (x)));
[hear] (element 0 (natural-set));
[hear] (element 0 (even-natural-set));
[hear] (element 1 (natural-set));
[hear] (not / element 1 (even-natural-set));
[hear] (element 2 (natural-set));
[hear] (element 2 (even-natural-set));
[hear] (element 3 (natural-set));
[hear] (not / element 3 (even-natural-set));
[hear] (element 4 (natural-set));
[hear] (element 4 (even-natural-set));
[hear] (element 5 (natural-set));
[hear] (not / element 5 (even-natural-set));
[hear] (element 6 (natural-set));
[hear] (element 6 (even-natural-set));
# MATH introduce graph structures
[hear] (define make-graph /
lambda (nodes links) (pair (nodes) (links)));
[hear] (define test-graph /
make-graph
(vector 1 2 3 4)
(vector (vector 1 2) (vector 2 3) (vector 1 4)));
[hear] (define graph-linked /
lambda (g n1 n2)
(exists /
? idx /
if (and (>= (idx) 0)
(< (idx) (list-length / list-ref (g) 1)))
(list= (list-ref (list-ref (g) 1) (idx))
(vector (n1) (n2)))
(false)));
[hear] (= (graph-linked (test-graph) 1 2) (true));
[hear] (= (graph-linked (test-graph) 1 3) (false));
[hear] (= (graph-linked (test-graph) 2 4) (false));
# 'if' is used a lot in the next definition in place of and / or
# this is because I haven't established lazy evaluation forms for and / or
# so this very inefficient algorithm completely bogs down when combined
# ... during testing with a dumb implementation for 'exists'.
[hear] (define graph-linked* /
lambda (g n1 n2)
(if (= (n1) (n2))
(true)
(if (graph-linked (g) (n1) (n2))
(true)
(exists
(? n3 /
if (graph-linked (g) (n1) (n3))
(graph-linked* (g) (n3) (n2))
(false))))));
[hear] (= (graph-linked* (test-graph) 1 2) (true));
[hear] (= (graph-linked* (test-graph) 1 3) (true));
[hear] (= (graph-linked* (test-graph) 2 4) (false));
# OBJECT introduce simple form of typing, for ease of documentation.
# An object is simply a function that takes an argument.
# The argument is the method to call on the object.
# Types are here taken to be just the existence of a particular method,
# with that method returning an object of the appropriate type.
[hear] (define make-integer
(lambda (v)
(lambda (x)
(if (= (x) int)
(v)
0))));
[hear] (define objectify
(? x
(if (number? (x))
(make-integer (x))
(x))));
[hear] (define instanceof
(lambda (T t)
(if (number? (t))
(= (T) int)
(not (number? ((objectify (t)) (T)))))));
# add version of lambda that allows types to be declared
[hear] (define prev-translate (translate));
[hear] (define translate
(let ((prev (prev-translate)))
(? x
(if (number? (x))
(prev (x))
(if (= (head (x)) lambda)
(let ((formals (head (tail (x))))
(body (head (tail (tail (x))))))
(if (> (list-length (formals)) 0)
(if (number? (last (formals)))
(translate
(vector
lambda
(except-last (formals))
(vector ? (last (formals)) (body))))
(let ((formal-name (first (last (formals))))
(formal-type (second (last (formals)))))
(translate
(vector
lambda
(except-last (formals))
(vector
?
(formal-name)
(vector
let
(vector (vector
(formal-name)
(vector
(vector objectify (vector (formal-name)))
(formal-type))))
(body)))))))
(translate (body))))
(prev (x)))))));
# add conditional form
[hear] (define prev-translate (translate));
[hear] (define translate
(let ((prev (prev-translate)))
(? x
(if (number? (x))
(prev (x))
(if (= (head (x)) cond)
(let ((cnd (head (tail (x))))
(rem (tail (tail (x)))))
(if (> (list-length (rem)) 0)
(translate
(vector
if
(first (cnd))
(second (cnd))
(prepend cond (rem))))
(translate (cnd))))
(prev (x)))))));
[hear] (= 99 (cond 99));
[hear] (= 8 (cond ((true) 8) 11));
[hear] (= 11 (cond ((false) 8) 11));
[hear] (= 7 (cond ((false) 3) ((true) 7) 11));
[hear] (= 3 (cond ((true) 3) ((true) 7) 11));
[hear] (= 11 (cond ((false) 3) ((false) 7) 11));
[hear] (define remove-match
(lambda (test lst)
(if (> (list-length (lst)) 0)
(if (test (head (lst)))
(remove-match (test) (tail (lst)))
(prepend (head (lst)) (remove-match (test) (tail (lst)))))
(lst))));
[hear] (define remove-element
(lambda (x)
(remove-match (lambda (y) (= (y) (x))))));
[hear] (list= (vector 1 2 3 5) (remove-element 4 (vector 1 2 3 4 5)));
[hear] (list= (vector 1 2 3 5) (remove-element 4 (vector 1 4 2 4 3 4 5)));
[hear] (define return
(lambda (T t)
(let ((obj (objectify (t))))
(obj (T)))));
[hear] (define tester
(lambda ((x int) (y int))
(return int (+ (x) (y)))));
[hear] (= 42 (tester (make-integer 10) (make-integer 32)));
[hear] (= 42 (tester 10 32));
[hear] (define reflective
(lambda (f)
((lambda (x)
(f (lambda (y) ((x (x)) (y)))))
(lambda (x)
(f (lambda (y) ((x (x)) (y))))))));
# OBJECT an example object -- a 2D point
[hear] (define point
(lambda (x y)
(reflective
(lambda (self msg)
(cond ((= (msg) x) (x))
((= (msg) y) (y))
((= (msg) point) (self))
((= (msg) +)
(lambda ((p point))
(point (+ (x) (p x))
(+ (y) (p y)))))
((= (msg) =)
(lambda ((p point))
(and (= (x) (p x))
(= (y) (p y)))))
0)))));
[hear] (define point1 (point 1 11));
[hear] (define point2 (point 2 22));
[hear] (= 1 (point1 x));
[hear] (= 22 (point2 y));
[hear] (= 11 ((point 11 12) x));
[hear] (= 11 (((point 11 12) point) x));
[hear] (= 16 (((point 16 17) point) x));
[hear] (= 33 (point1 + (point2) y));
[hear] (point1 + (point2) = (point 3 33));
[hear] (point2 + (point1) = (point 3 33));
[hear] ((point 100 200) + (point 200 100) = (point 300 300));
[hear] (instanceof point (point1));
[hear] (not (instanceof int (point1)));
[hear] (instanceof int 5);
[hear] (not (instanceof point 5));
# OBJECT an example object -- a container
[hear] (define container
(lambda (x)
(let ((contents (make-cell (vector))))
(reflective
(lambda (self msg)
(cond ((= (msg) container) (self))
((= (msg) inventory) (get! (contents)))
((= (msg) add)
(lambda (x)
(if (not (element (x) (get! (contents))))
(set! (contents) (prepend (x) (get! (contents))))
(false))))
((= (msg) remove)
(lambda (x)
(set! (contents) (remove-element (x) (get! (contents))))))
((= (msg) =)
(lambda ((c container))
(set= (self inventory) (c inventory))))
0))))));
# Can pass anything to container function to create an object
# Should eventually use a consistent protocol for all objects,
# but all this stuff is still in flux
[hear] (define pocket (container new));
[hear] (pocket add 77);
[hear] (pocket add 88);
[hear] (pocket add 99);
[hear] (set= (pocket inventory) (vector 77 88 99));
[hear] (pocket remove 88);
[hear] (set= (pocket inventory) (vector 77 99));
[hear] (define pocket2 (container new));
[hear] (pocket2 add 77);
[hear] (pocket2 add 99);
[hear] (pocket2 = (pocket));
# OBJECT expressing inheritance
# counter-container adds one method to container: count
[hear] (define counter-container
(lambda (x)
(let ((super (container new)))
(reflective
(lambda (self msg)
(cond ((= (msg)