; 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)