PFPL Chapter 3 Hypothetical and General Judgments

Posted on In Disqus:

Please refer this link from page 23 to 32.

Keywords

  • Hypothetical Judgments: an entailment between one or more hypotheses and a conclusion.
  • Entailment has 2 notions:
    • derivability
    • admissibility
  • General Judgment: the universality or genericity of a judgment.
  • General Judgment has 2 forms:
    • generic
    • parametric

Hypothetical Judgments

Some notations:

  • $\Delta$ or $\Gamma$ to stand for a finite set of basic judgments.
  • $\mathcal{R}$ stands for a finite set of rules.
  • $\vdash$ stands for derivability.
  • $\vdash_\mathcal{R}$ stands for derivable under set of rules $\mathcal{R}$.
  • $\vDash$ stands for admissibility.
  • $\vDash_\mathcal{R}$ stands for admissible under set of rule $\mathcal{R}$.

Derivability

The derivability judgment is defined by $\mathrm J_1,\dots,\mathrm J_k \vdash_R K$, where $\mathrm J_i$ and $K$ are basic judgments.

In another word, we can derive $K$ from the expansion $R \cup {J_1,\dots,J_k }$ of rule set $R$ with axioms

$$
\dfrac{}{\mathrm J_1}, \dots, \dfrac{}{\mathrm J_k}
$$

An equivalent way to see this is to say that

$$
\dfrac{J_1\dots J_n}J
$$

is derivable from $R$.

Stability

If $\Gamma \vdash_R J$, then $\Gamma \vdash_{R\cup R’} J$.

Reflexivity

Every judgment is a consequence of itself: $\Gamma, J\vdash_R J$. Every hypothesis justifies itself as conclusion.

Weakening

If $\Gamma \vdash_R J$, then $\Gamma, K \vdash_R J$. Entailment is not influenced by un-exercised options.

Transitivity

If $\Gamma, K \vdash_R J$ and $\Gamma \vdash_R K$, then $\Gamma \vdash_R J$.

Admissibility

A weaker form of hypothetical judgment than derivability, written as $\Gamma \vDash_R J$.

It is stating that $\vdash_R \Gamma$ implies $\vdash_R J$.

If any of hypotheses are not derivable by $R$, then it is vacuously true.

An equivalent way to see this is to say that
$$
\dfrac{J_1\dots J_n}J
$$
is admissible relative to the rules in $R$.

Weaker Form

If $\Gamma \vdash_R J$, then $\Gamma \vDash_R J$

Reflexivity

$J\vDash_R J$

Weakening

If $\Gamma \vDash_R J$, then $\Gamma, K \vDash_R J$

Transitivity

If $\Gamma, K \vDash_R J$ and $\Gamma \vDash_R K$, then $\Gamma \vDash_R J$

Structural Properties of Entailment

$\Gamma \vDash_R J$ enjoys the structural properties of entailment.

Differences between Derivability and Admissibility

Derivability Admissibility
Stable under extension with new rules. Not stable with new rules extension. (Strongest & Closed-Under)
Get evidence by composing rules Get evidence by composing and induction

Hypothetical Inductive Definitions

Some notations:

  • $\Gamma$ as global hypotheses
  • $\Gamma_i$ as local hypothesis for $i^{th}$ premise of some rule

Enrich the concept of inductive definition to allow rules with derivability judgments as premises and conclusions.

Local Hypothesis is applied only in derivation of a particular premise, like the $\Gamma_i$ in $\Gamma \Gamma_i \vdash J_i$.

Hypothetical inductive definition has a following form
$$
\dfrac{\Gamma \Gamma_1 \vdash J_1, \dots, \Gamma \Gamma_n \vdash J_n}{\Gamma \vdash J}
$$
We require all rules in hypothetical inductive definition be uniform (so to say they can be applied in all global contexts). Then we have a implicit or local form
$$
\dfrac{\Gamma_1 \vdash J_1, \dots, \Gamma_n \vdash J_n}{J}
$$
A hypothetical inductive definition is regarded as an inductive definition of a formal deriviability judgment $\Gamma \vdash J$.

A set of hypothetical rules $R$ defines the strongest formal derivability judgment that is structural and closed under uniform rules $R$. (closed and strongest please refer here).

Structural/Structurality means that the formal derivability judgment must be closed under the rules:
$$
\dfrac{}{\Gamma, J \vdash J}
$$

$$
\dfrac{\Gamma \vdash J}{\Gamma, K \vdash J}
$$

$$
\dfrac{\Gamma \vdash K\phantom{“”}\Gamma, K \vdash J}{\Gamma \vdash J}
$$

Principle of hypothetical rule induction is just the principle of rule induction applied to the formal hypothetical judgment.

So to show $P(\Gamma \vdash J)$ when $\Gamma \vdash_R J$, it is enough to show that $P$ is closed under the rules of $R$ and the structural rules.

We use admissibility method to dispense structural rules in practice.

To prove that structural rules are admissible by rule induction may restrict rules in $R$.

If all rules in $R$ are uniform, then the latter 2 structural rules are admissible.

The first structural rule must be stated explicitly as a rule.

General Judgments

Some notations:

  • $\Gamma \vdash^{\mathcal{U;X}}_\mathcal {R} J$ stands for $J$ is derivable from $\Gamma$ according to rule $\mathcal R$, with objects consisting of abt’s over symbol $\mathcal U$ and variables $\mathcal R$.

General judgments codify the rules for handling variables in a judgment.

  • A generic judgment states that a judgment holds for any choice of objects replacing designated variables in original judgment. (generality wrt all substitution instances for variables in a judgment)
  • A parametric judgment expresses generality over any fresh renaming of designated symbols in a judgment.

Extended Concept of Uniformity

The concept of uniformity of rules is extended to require that the rules be

  • closed under renaming and substitution of variables
  • closed under renaming for parameters

If $\mathcal R$ is a set of rules including free variable $x$ of sort $s$ , then it should include all possible substitution instances of abt’s $a$ of sort $s$ for $x$.

Similarly, if $\mathcal R$ contains rules with a parameter $u$, then it must contain all instances that rules substitute $u$ with $u’$ of same sort.

Uniformity rules out stating a rule for a variable/parameter.

Generic and Parametric Derivability

Generic Derivability

Generic derivability is defined as
$$
\mathcal Y\ |\ \Gamma \vdash^\mathcal X_R \iff \Gamma \vdash ^{\mathcal{X} \mathcal Y}_R J
$$
where $\mathcal Y \cap \mathcal X = \varnothing$.

The evidence of generic derivability consist of a generic derivation $\triangledown$ involving variables $\mathcal X \ \mathcal Y$.

Structural Properties of Generic Derivability

So long as $\mathcal R$ is uniform, the following structural properties governs the behavior of variables.

Proliferation

If $\mathcal Y \ | \ \Gamma \vdash^\mathcal X_\mathcal R J$, then $\mathcal Y, \mathcal y \ | \ \Gamma \vdash^\mathcal X_\mathcal R J$

Renaming

If $\mathcal Y, \mathcal y \ | \ \Gamma \vdash^\mathcal X_\mathcal R J$, then $\mathcal Y, \mathcal y’ \ | \ [y \leftrightarrow y’]\Gamma \vdash^\mathcal X_\mathcal R [y \leftrightarrow y’]J$ for any $y \notin \mathcal X\ \mathcal Y$

Substitution

If $\mathcal Y, \mathcal y \ | \ \Gamma \vdash^\mathcal X_\mathcal R J$ and $a \in \mathcal B[\mathcal X\ \mathcal Y]$, then $\mathcal Y\ | \ [a/y]\Gamma \vdash^\mathcal X_\mathcal R [a/y]J$

Parametric Derivability

Parametric derivability is defined as
$$
\mathcal V \ \parallel\ \mathcal Y\ |\ \Gamma \vdash^{\mathcal U;\mathcal X}_R J \iff \mathcal {Y}\ |\ \Gamma \vdash_R^{\mathcal{UV;X}} J
$$
where $\mathcal U \cap \mathcal V = \varnothing$

Generic Inductive Definitions

A generic rule has form
$$
\dfrac{\mathcal Y\ \mathcal Y_1\ |\ \Gamma\ \Gamma_1 \vdash J_1\ \dots\ \mathcal Y\ \mathcal Y_n\ |\ \Gamma\ \Gamma_n \vdash J_n}{\mathcal Y\ |\ \Gamma \vdash J}
$$
and implicit form
$$
\dfrac{\mathcal Y_1\ |\ \Gamma_1 \vdash J_1\ \dots\ \mathcal Y_n\ |\ \Gamma_n\vdash J_n}{J}
$$
To ensure that the formal generic judgments behaves like a generic judgment, we must ensure the structural rules are admissible
$$
\dfrac{}{\mathcal Y\ |\ \Gamma, J\vdash J}
$$

$$
\dfrac{\mathcal Y\ |\ \Gamma \vdash J}{\mathcal Y\ |\ \Gamma, J’ \vdash J}
$$

$$
\dfrac{\mathcal Y\ |\ \Gamma \vdash J}{\mathcal Y, x\ |\ \Gamma \vdash J}
$$

$$
\dfrac{\mathcal Y, x’\ |\ [x \leftrightarrow x’]\Gamma \vdash [x \leftrightarrow x’]J}{\mathcal Y, x\ |\ \Gamma \vdash J}
$$

$$
\dfrac{\mathcal Y\ |\ \Gamma \vdash J \phantom{“”} \mathcal Y\ |\ \Gamma, J \vdash J’}{\mathcal Y\ |\ \Gamma \vdash J’}
$$

$$
\dfrac{\mathcal Y, x\ |\ \Gamma \vdash J\phantom{“”}a \in \mathcal B[\mathcal Y]}{\mathcal Y\ |\ [a/x]\Gamma \vdash [a/x]J}
$$

The last rule must be verified explicitly for each inductive definition.

Exercise

3.1

$$
\dfrac{\text{s comb}}{\text{len(s, 1)}}\phantom{“”}\dfrac{\text{k comb}}{\text{len(k, 1)}}
$$

$$
\dfrac{a_1\text{ comb}\phantom{“”}n_1\text{ nat}\phantom{“”}\text{len}(a_1, n_1)}{\text{len}(\text{ap}(a_1;\text{s}), \text{succ}(n_1))}
$$

$$
\dfrac{a_1\text{ comb}\phantom{“”}n_1\text{ nat}\phantom{“”}\text{len}(a_1, n_1)}{\text{len}(\text{ap}(a_1;\text{k}), \text{succ}(n_1))}
$$

$$
\dfrac{a_2\text{ comb}\phantom{“”}n_2\text{ nat}\phantom{“”}\text{len}(a_2, n_2)}{\text{len}(\text{ap}(\text{s};a_2), \text{succ}(n_2))}
$$

$$
\dfrac{a_2\text{ comb}\phantom{“”}n_2\text{ nat}\phantom{“”}\text{len}(a_2, n_2)}{\text{len}(\text{ap}(\text{k};a_2), \text{succ}(n_2))}
$$

3.2

  • Rename $x’$ of $x$ and extend the $\mathcal C$ with rule $a’ \text{comb}$.
  • Substitute $x’$ with $a_1$ if $x’$ occurs, otherwise proceed inductively.

3.3

$$
\text{s k k x} \equiv (\text{k x}) (\text{k x}) \equiv \text x
$$

3.4

Consider $[x]a$ with fixed $x$ as argument, i.e., $([x]a) x$

The bracket abstraction can be defined by following rules
$$
\dfrac{}{[x]x \equiv \text{s k k}}
$$

$$
\dfrac{}{[x]\text k \equiv \text{k k}}
$$

$$
\dfrac{}{[x]\text s \equiv \text{k s}}
$$

$$
\dfrac{[x]a_1 \equiv a_1’\phantom{“”}[x]a_2 \equiv a_2’}{[x]a_1 a_2 \equiv \text{s }([x]a_1) \ ([x]a_2)}
$$

3.5

According to Prof. Harper, if we use the definition of $[x] a$ in 3.4, then we will get a big mass on left hand side: $[a/y]$$([x]b)$. Consider the case when $b$ is $y$, then it will reconstruct $a$ when $x$ is applied but it will be a big mass.

So the main point is to construct a more efficient abstraction algorithm here for SKI combinator and avoid messing with parts without $x$. Say, $[x]a \triangleq \text{ap}(\text{k}; a)$ when $x \notin a$.

Related links:

3.6

  • $\mathcal B[\mathcal X]$ of abt’s is generated by
    • operator $\text{ap}$ with arity (Exp, Exp) Exp
    • operator $\lambda$ with arity (Exp.Exp) Exp
    • $\mathcal X$ set of variables with sort Exp

So for $b \text{ closed}$ with no occurrences of variables in $\mathcal X$, we define following inductive rules
$$
\dfrac{1 \leq i \leq n}{x_1, \dots, x_k\ |\ x_1 \text{ closed}, \dots, x_k\text{ closed}\ \vdash x_i \text{ closed}}
$$

$$
\dfrac{x_1, \dots, x_k\ |\ x_1 \text{ closed}, \dots, x_k\text{ closed}\ \vdash a_1 \text{ closed}\phantom{“”}x_1, \dots, x_k\ |\ x_1 \text{ closed}, \dots, x_k\text{ closed}\ \vdash a_2 \text{ closed}}{x_1, \dots, x_k\ |\ x_1 \text{ closed}, \dots, x_k\text{ closed}\ \vdash \text{ap}(a_1;a_2) \text{ closed}}
$$

$$
\dfrac{x_1, \dots, x_k\ |\ x_1 \text{ closed}, \dots, x_k\text{ closed}, x \text{ closed}\ \vdash a \text{ closed}}{x_1, \dots, x_k\ |\ x_1 \text{ closed}, \dots, x_k\text{ closed}\ \vdash \lambda(x.a) \text{ closed}}
$$

We need to require that these local variables $x_1, \dots, x_k$ are disjoint to $\mathcal X$.