You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I was going through the Recess section on J-Bob, starting on page 164, when I noticed that some of the Scheme examples in little-prover.scm give incorrect results when run in MITScheme/DrRacket, but their ACL2 equivalents in little-prover.lisp give correct results when run in ACL2/DrRacket. I ran the first five Chapter 1 examples in both MIT/GNU Scheme and Dr Racket using R5RS (as described in the README) - the REPL dialogue in both interpreters proceeded as follows:
$ (load "j-bob/scheme/j-bob-lang.scm")
$ (load "j-bob/scheme/j-bob.scm")
$ (load "j-bob/scheme/little-prover.scm")
$ (chapter1.example1) ;;
-> (car (cons 'ham '(eggs))) ;; INCORRECT; should be 'ham
$ (chapter1.example2)
-> 't ;; CORRECT
$ (chapter1.example3)
-> (atom (cons 'ham '(eggs))) ;; INCORRECT; should be 'nil
$ (chapter1.example4)
-> 'nil ;; CORRECT
$ (chapter1.example5)
-> (equal 'flapjack (atom (cons a b))) ;; INCORRECT; should be 'nil
I noticed that the correct and incorrect examples differ in one key respect: the correct examples have no path to the focus (i.e., the focus is the entire expression) in their definitions, whereas the incorrect examples have at least one step with a path to the focus. Here's the same Chapter 1 examples, run with the ACL2 Dracula package in Dr Racket, showing correct output for all examples:
Diagnosing why this is occurring is beyond my abilities at this point - can one of the authors, or someone who is more well-versed in Scheme/LISP than I am, explain what's going on here?
The text was updated successfully, but these errors were encountered:
I was going through the Recess section on J-Bob, starting on page 164, when I noticed that some of the Scheme examples in little-prover.scm give incorrect results when run in MITScheme/DrRacket, but their ACL2 equivalents in little-prover.lisp give correct results when run in ACL2/DrRacket. I ran the first five Chapter 1 examples in both MIT/GNU Scheme and Dr Racket using R5RS (as described in the README) - the REPL dialogue in both interpreters proceeded as follows:
$ (load "j-bob/scheme/j-bob-lang.scm")
$ (load "j-bob/scheme/j-bob.scm")
$ (load "j-bob/scheme/little-prover.scm")
$ (chapter1.example1) ;;
-> (car (cons 'ham '(eggs))) ;; INCORRECT; should be 'ham
$ (chapter1.example2)
-> 't ;; CORRECT
$ (chapter1.example3)
-> (atom (cons 'ham '(eggs))) ;; INCORRECT; should be 'nil
$ (chapter1.example4)
-> 'nil ;; CORRECT
$ (chapter1.example5)
-> (equal 'flapjack (atom (cons a b))) ;; INCORRECT; should be 'nil
I noticed that the correct and incorrect examples differ in one key respect: the correct examples have no path to the focus (i.e., the focus is the entire expression) in their definitions, whereas the incorrect examples have at least one step with a path to the focus. Here's the same Chapter 1 examples, run with the ACL2 Dracula package in Dr Racket, showing correct output for all examples:
$ (include-book "j-bob-lang" :dir :teachpacks)
$ (include-book "j-bob" :dir :teachpacks)
$ (include-book "little-prover" :dir :teachpacks)
$ (chapter1.example1)
-> 'ham ;; CORRECT
$ (chapter1.example2)
-> 't ;; CORRECT
$ (chapter1.example3)
-> 'nil ;; CORRECT
$ (chapter1.example4)
-> 'nil ;; CORRECT
$ (chapter1.example5)
-> 'nil ;; CORRECT
Diagnosing why this is occurring is beyond my abilities at this point - can one of the authors, or someone who is more well-versed in Scheme/LISP than I am, explain what's going on here?
The text was updated successfully, but these errors were encountered: