PLT Redex: how to falsify the judgment in define-judgment-form

20 views
Skip to first unread message

Xu Xue

unread,
Jan 3, 2021, 3:59:48 AM1/3/21
to Racket Users
Hi, Racketeers

Since Redex can calculate all possible results in the judgment, Can I add some negative premise to help derive the output? like

(define-judgment-form Lambda
#:mode (infer I O)
[(infer A B)
(not (infer number B)
---------------------
(Infer C B)]

I tried to replace bold line with (side-condition (not (judgment-holds (infer number B)))), which is disallowed in Redex since B is in the output position.

So any standard way to express this intention?


Regards
Xu

Robby Findler

unread,
Jan 3, 2021, 10:47:50 AM1/3/21
to Xu Xue, Racket Users

I think this boils down to a question about how redex executes judgment forms. Leaving aside modeless judgment forms (where redex will only check a derivation for you but won't ever make them up), redex is turning each judgment form into a (fancy) function from the inputs to sets of the outputs and, based on how that function goes, will build a derivation for you.

So, in the example in your message, think of `infer` as a function that consumes the first thing and produces the second thing, where the part below the bar is a kind of case/choice and the part above the bar are recursive calls. So, if we want to use that rule, we'll be given "C" and have to come up with "B". To make the recursive call to infer for the premise, we have to supply an "A" which will then give us a "B". And now we're stuck because we don't have that "B".

Of course, there are many other ways that one could think of turning judgment forms into something that is, at least in some sense, executable. Doing something like prolog is an obvious choice (although Redex is more expressive than the standard/original prolog so there are some tricks required) and Redex does indeed use a prolog-inspired solver when it is generating random derivations that satisfy a judgment form (see Burke Fetscher's dissertation). One might also try to turn it into a SMT query, but Redex doesn't currently do that (and there aren't any plans to do that). Perhaps there is another way too.

So, as to your specific question, the answer is "it depends". If you can formulate your judgment form in a way that respects the mode, then yes, you can use premises to constrain the sets of valid judgments. If not, you can't.

hth,
Robby


--
You received this message because you are subscribed to the Google Groups "Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/25e4ec2e-ba34-4a53-8284-37cbac422ae2n%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages