Re: [racket-users] PLT Redex: how to falsify the judgment in define-judgment-form

[Robby Findler]

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


On Sun, Jan 3, 2021 at 2:59 AM Xu Xue  wrote:

> 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?
>
> more concrete example is in
> https://github.com/juniorxxue/applicative-intersection-semantics/blob/main/definition.rkt#L94
>
> Regards
> Xu
>
> --
> 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+unsubscr...@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
> 
> .
>

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/racket-users/CAL3TdONOr5pJCtmH53bT-7tH3OuyVeKm_P61M0KSAegsx%3DQa%3Dg%40mail.gmail.com.

[racket-users] PLT Redex: how to falsify the judgment in define-judgment-form

[Xu Xue]

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?

more concrete example is in 
https://github.com/juniorxxue/applicative-intersection-semantics/blob/main/definition.rkt#L94

Regards
Xu

-- 
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+unsubscr...@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.