Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Scheme J-Bob/step examples w/ non-null focus paths return incorrect results; ACL2 equivalents return correctly. #6

Closed
ghost opened this issue May 11, 2016 · 2 comments

Comments

@ghost
Copy link

ghost commented May 11, 2016

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?

@ghost
Copy link
Author

ghost commented May 11, 2016

Never mind, I foolishly neglected to update my repo - including commit 1f68e43 fixed this issue.

@ghost ghost closed this as completed May 11, 2016
@carl-eastlund
Copy link
Contributor

Glad to see the issue is fixed, sorry for the initial difficulties. Happy proving!

This issue was closed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant