Someone's Intermediate Representation

0%

# Keywords

• Hypothetical Judgments: an entailment between one or more hypotheses and a conclusion.
• Entailment has 2 notions:
• derivability
• 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​$.

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

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)}$$