3.17 Problem: Binary Addition
Redex can also model hardware scenarios.
Here is a language of bit expressions:
(define-language L (e ::= (or e e) (and e e) (not e) (append e ...) (add e e) v) (v ::= (b ...)) (b ::= 0 1) (n ::= natural))
Your task is to design a standard reduction system that mimics addition on
sequences of bits (binary digits).
Hints Raw values are sequences of booleans, not just one. For or, you can reduce sequences that have more than one element into appends of ors that each have a single element, and then actually handle or’s logic for arrays that have just one element. This also works for and and not. This idea doesn’t work for add.
Here are some test cases to get you started:
(module+ test (test-->> red (term (or (1 1 0 0) (0 1 0 1))) (term (1 1 0 1))) (test-->> red (term (not (0 1))) (term (1 0))) (test-->> red (term (append (1 0) (0 1))) (term (1 0 0 1))) (test-->> red (term (or (1 1 0 0) (0 1 0 1))) (term (1 1 0 1))) (test-->> red (term (and (1 1) (0 1))) (term (0 1))) (test-->> red (term (and (0 0) (0 1))) (term (0 0))))
For testing add, we suggest comparing it to Racket’s +
operation using this helper function:
; v -> n (in L) ; convert a sequence of bits to a natural number (module+ test (test-equal (to-nat (term ())) 0) (test-equal (to-nat (term (0))) 0) (test-equal (to-nat (term (1))) 1) (test-equal (to-nat (term (0 1))) 1) (test-equal (to-nat (term (1 0))) 2) (test-equal (to-nat (term (1 1))) 3) (test-equal (to-nat (term (1 1 1))) 7) (test-equal (to-nat (term (0 1 1 1))) 7) (test-equal (to-nat (term (0 1 1 0))) 6)) (define (to-nat bs) (for/sum ([b (in-list (reverse bs))] [i (in-naturals)]) (* b (expt 2 i))))