Brainfuck/w/index.php?title=Talk:Brainfuck/index.php

Brainfuck/w/index.php?title=Talk:Brainfuck/index.php is a language invented by User:ehird in a newly-awaken stupor in late 2010. The language is identical to brainfuck without input or output in every way, except that only programs that halt are valid. That is, the set of programs P is defined in terms of the set of brainfuck programs BF like so:

P = {p ∈ BF : (',' ∉ p) ∧ ('.' ∉ p) ∧ halts(p)}

where halts(p) is, of course, only well-defined for programs without input. (Any brainfuck halting-checker function could be used by passing an irrelevant constant input; since Brainfuck/w/index.php?title=Talk:Brainfuck/index.php programs cannot do IO, this is equivalent.)

Implementations are strongly recommended to flag an error whenever a program in BF but not in P is given, but strictly, like all handling of invalid programs, what they do is undefined behaviour.

Implementation

This implementation, in Scheme-1, satisfies the error recommendation above. It defines a procedure run which takes a pre-parsed Brainfuck/w/index.php?title=Talk:Brainfuck/index.php program as an argument, and returns (before . after), where before is the tape before the pointer, and after is the tape at the pointer and after, when the program ended.

The pre-parsed form maps the instructions +, -, < and > to symbols with those names, and maps [body] to (body′), where body′ is the pre-parsed form of body. The program itself is a list of its pre-parsed instructions.

The interpreter has a right-infinite tape of arbitrarily large integers.

(define interpret-code
  '(cond
    ((null? p) (cons before after))
    ((list? (car p))
     (if (= (car after) 0)
         (interpret (cdr p) before after)
         (let ((result (interpret (car p) before after)))
           (interpret p (car result) (cdr result)))))
    (else
     (case (car p)
       ('+ (interpret (cdr p) before (cons (+ (car after) 1) (cdr after))))
       ('- (interpret (cdr p) before (cons (- (car after) 1) (cdr after))))
       ('< (interpret (cdr p) (cdr before) (cons (car before) after)))
       ('> (interpret (cdr p) (cons (car after) before) (cdr after)))))))

(define (interpret p before after)
  ((eval
   `(letrec ((interpret (lambda (p before after) ,interpret-code)))
      interpret)
   (interaction-environment))
   p before after))

(define (run p)
  (let ((zeroes (list 0)))
    (set-cdr! zeroes zeroes)
    (if (H 0
           `(letrec ((interpret (lambda (p before after) ,interpret-code))
                     (zeroes (list 0)))
              (set-cdr! zeroes zeroes)
              (interpret ',p '() zeroes)))
        (interpret p '() zeroes)
        (error "That's no program!"))))

Computational class

The defined behavior of the language can compute the set of total computations (that is, take the set R of all total functions, pick some fixed value n, and give all the functions n for input instead of allowing it to vary.)

Since it is not defined what an implementation must do if presented with a non-halting program, however, an implementation is not prohibited from running it as brainfuck would, and in this sense, the definition of Brainfuck/w/index.php?title=Talk:Brainfuck/index.php does not exclude Turing-complete computations.