; Proving by construction that R5RS macros with the removed ability
; to generate other macros are still Turing-complete.
; This limited form of R5RS macros preserves the
; hygiene condition for macro expansions, as defined in KFFD86:
; "Generated identifiers that become binding instances in
; the completely expanded program must only bind variables that are
; generated at the same transcription step."
;
; $Id: turing-completeness-limited-macros.scm,v 1.1 2003/09/16 04:58:03 oleg Exp oleg $
; The alphabet is a subset of Scheme character or numeric literals.
; #f is reserved to denote a blank cell. We will model Turing
; machine's tape by two lists. The first list enumerates symbols on
; the tape on the left of the head: from the symbol in the cell
; immediately to the left all the way to the first cell of the tape.
; The list appears to be "in reverse".
; The second list contains the current and the following symbols (to
; the right of the head). The second list is conceptually
; infinite. However, the infinite sequence of the blank cells will
; only be assumed. The infinite tape is thus modeled by a finite
; string of tokens followed by an _assumed_ infinite sequence of blank
; cells. We will never write out this tail of blanks explicitly;
; rather we will assume that there is always a blank cell after the
; right end of every finite string under re-writing.
;
; For example, a pair of lists
; (2 1 #f) (3)
; stands for a Turing machine configuration with a tape
; containing a blank, followed by a symbol '1' then symbol '2' and then
; symbol '3'. The read/write head is over the symbol '3'.
; A pair of lists (1 1) (#f)
; represents a tape with two non-blank symbols ('1') at the very
; beginning; the head is pointing to the first blank after them.
; Each ruleset in the machine's finite control is represented by
; a macro of the form
; (ruleset-macro tape-left tape-right)
; The macro should expand into the invocation of another ruleset macro
; (or of the same ruleset macro), or a special macro 'halt'.
; Program 1: Addition of natural numbers. Two numbers to add are encoded
; in unary, in the following format
; #f n1 #f n2 #f
; where n1 is a sequence of zero or more tokens '1' corresponding to the
; first number to add (in unary notation), n2 stands for the second
; number. The numbers are terminated with a blank cell; the head is at
; the blank cell that terminates the second number. The algorithm is
; simple: move the head left until it hits the blank separating the two
; numbers, replace this blank with token '`', move the head right to the
; first blank, replace the previous token with the blank, and
; stop. Here's the corresponding program
; Search left for the blank that separates the numbers
; If found, replace the blank with 1, and switch to state rs-add-sr
(define-syntax rs-add-sl
(syntax-rules ()
((rs-add-sl left (#f . right))
(rs-add-sr left (1 . right)))
((rs-add-sl (x . left) right)
(rs-add-sl left (x . right)))))
; Scan right for the blank
(define-syntax rs-add-sr
(syntax-rules ()
((rs-add-sr (x . left) (#f . right))
(halt left (#f . right)))
; there is always blank at the right edge of the tape
((rs-add-sr left ())
(rs-add-sr left '(#f)))
((rs-add-sr left (x . right))
(rs-add-sr (x . left) right))))
; make the initial move left
(define-syntax rs-add
(syntax-rules ()
((rs-add (x . left) right)
(rs-add-sl left (x . right)))))
(define-syntax halt
(syntax-rules ()
((halt tape-left tape-right)
(display (list (reverse (quote tape-left)) (quote tape-right))))))
(display "rs-add") (newline)
; 2 + 3
(rs-add (1 1 1 #f 1 1 #f) (#f))
(newline)
; 2 + 0
(rs-add (#f 1 1 #f) (#f))
(newline)
; 0 + 2
(rs-add (1 1 #f #f) (#f))
(newline)
; 0 + 0
(rs-add (#f #f) (#f))
(newline)
; Program 2: A decision machine. Decide if the number of tokens on the
; tape between two delimiting blanks is even or odd. The program is
; self-explanatory.
(define-syntax rs-evenp
(syntax-rules ()
((rs-evenp (#f . left) (#f . right))
(halt ("YES" #f . left) (#f)))
((rs-evenp (x . left) (#f . right))
(rs-oddp left (#f . right)))))
(define-syntax rs-oddp
(syntax-rules ()
((rs-oddp (#f . left) (#f . right))
(halt ("NO" #f . left) (#f)))
((rs-oddp (x . left) (#f . right))
(rs-evenp left (#f . right)))))
(display "rs-evenp") (newline)
; 0
(rs-evenp (#f) (#f))
(newline)
; 1
(rs-evenp (1 #f) (#f))
(newline)
; 2
(rs-evenp (1 1 #f) (#f))
(newline)
; 3
(rs-evenp (1 1 1 #f) (#f))
(newline)
; 0
(rs-oddp (#f) (#f))
(newline)
; 1
(rs-oddp (1 #f) (#f))
(newline)
; 2
(rs-oddp (1 1 #f) (#f))
(newline)
; 3
(rs-oddp (1 1 1 #f) (#f))
(newline)
(exit)