2
$\begingroup$

I'm confused about the intended meaning of the following passage from Bob Harper's Practical Foundations for Programming Languages:

A collection of rules is considered to define the strongest judgment form that is closed under, or respects, those rules.

The author goes on to explain the italicized words.

Is this to be understood as saying that a collection of rules defines a unique judgment which somehow encompasses all judgments derivable from those rules?

If so- of what does this unique judgment consist? Does this necessarily include formal hypothetical judgments? Does it include some kind of union/conjunction of "orthogonal" applications of the rules? (eg $\overline{\text{zero nat}}$ and $\overline{\text{zero even}}$)

If not- what's the correct interpretation?

$\endgroup$
3
$\begingroup$

The interpretation of such paragraph is that rules define judgements. It's more or less the same as saying
closure: the judgment satisfies this rules
strongest: ..and this is all there is

So, for example, if you have the following two rules to define the judgement "to be a nat":

$$\frac{}{\mbox{zero nat}} \quad \frac{x \mbox{ nat}}{\mbox{suc(} x\mbox{) nat}}$$

then you are stating that:

closed:

  • $\mbox{zero}$ is a $\mbox{nat}$ and
  • if $x$ is a $\mbox{nat}$, then $\mbox{suc}(x)$ is a $\mbox{nat}$

strongest: no other word is a $\mbox{nat}$

$\endgroup$
  • 1
    $\begingroup$ i think you've answered my question, which was really about the absence of pluralization of "judgement form(s)", and not about being the strongest or closed. What i'm understanding from your answer is that the judgement forms of the system in question are defined as exactly those which appear in the rules. $\endgroup$ – afsmi Oct 29 '16 at 2:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.