Feature request: explicit derivations for moded judgments

[wilbowma]

Just noticed that you introduced modeless judgments and the ability to check explicit derivations. Nice!

But what if I want to check an explicit derivation on a moded judgment? This is useful when teaching and when debugging judgments I think ought to hold but Redex claims do not.

(Would be particularly useful if judgment-holds could tell me which step in a derivation didn't hold, instead of just giving #f, but I could probably construct that feature in user-land)

[rfindler]

How about using build-derivations?

As for the "try to make as big a derivation as you can", I've long thought that would be nice to have, but it isn't a trivial problem (given the way Redex already works).

[wilbowma]

(1) I want to be able to manually construct the derivation for a moded judgment, and give it to Redex to check. Even if Redex could compute the derivation, maybe I want to do it by hand to check my intuition.

(2) I wasn't thinking of "try to make as bug a derivation as you can", so much as "given a derivation, check each sub-derivation and report the first step that doesn't hold".

Something like...

;; completely untested
(define (check-derivation name d)
  (let loop ([ls (derivation-subs d)])
    (if (null? ls)
        (judgment-holds name d)
        (begin
          (for ([d ls])
            (unless (check-derivation name d)
              (error "sub-derivation ~a ~a failed!" (derivation-name d) d)))
          (unless (judgment-holds name d)
            (error "sub-derivation ~a ~a failed!" (derivation-name d) d)))

[wilbowma]

I tested that code and created a variant that works. I'll probably polish this a little more and submit a pull request.

(require (for-syntax racket/base syntax/parse))
(define-syntax (check-derivation stx)
  (syntax-parse stx
    [(_ name:id d)
     #`(let ([f (lambda (x) (judgment-holds name x))]
             [x d])
         (derivation-checker f x))]))

(define (derivation-checker f d)
  (let ([ls (derivation-subs d)])
    (if (null? ls)
        (f d)
        (begin
          (for ([d ls])
            (unless (derivation-checker f d)
              (error 'check-derivation "sub-derivation ~a ~a failed!" (derivation-name d) d)))
          (unless (f d)
            (error 'check-derivation "sub-derivation ~a ~a failed!" (derivation-name d) d))))))

[rfindler]

I understand now. Thanks for explaining.

It seems to me that this should be either an extension to test-judgment-holds or a new form with a name starting something like test-judgment-... and it should cooperate with the testing stuff that's already in redex. Maybe it should be test-derivation and it should accept both modeless and moded judgment forms but do what test-judgment-holds for modeless ones (and then do the same thing for modeless ones)?

[wilbowma]

Good idea

[wilbowma]

Regarding (1), by using build-derivations, did you mean basically check my manual derivation against the set generated by build-derivations?

That's not a bad work around, but seems a little indirect, and likely to have worse performance than necessary.

[rfindler]

Yes that could be expensive.

In practice for systems that don't have a lot of different ways to build the intermediate proofs it will be as efficient as redex can do, but if there are lots of candidates at the intermediate points it could end up being very slow for sure (like exponential in the size of the final derivation isn't hard to imagine). If it were inside the library (in a "test-..." form or some other "check this derivation" function), we could avoid that slowness.

Robby

On Thu, Oct 3, 2019 at 4:53 PM William J. Bowman notifications@github.com wrote:

Regarding (1), by using build-derivations, did you mean basically check my manual derivation against the set generated by build-derivations?

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/racket/redex/issues/198?email_source=notifications&email_token=AADBNMBWJPP36HE2543KQC3QMZSXHA5CNFSM4I4CVYX2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEAJW25Q#issuecomment-538144118, or mute the thread https://github.com/notifications/unsubscribe-auth/AADBNMA4XWLXRMNSZEYH5YTQMZSXHANCNFSM4I4CVYXQ .

[wilbowma]

Here's a terrible hack for (1)

(define (check-moded-derivation d)
  (set-member?
   (eval `(build-derivations ,(derivation-term d)))
   d))

I looked at the internals of judgment-holds/derivations, but it hasn't occurred to me how to do what I want. I'll probably create a variant of test-derivations that does both things and worry about performance later.

[wilbowma]

Working on this in the test-derivation branch.