Please refer this link from page 23 to 32.

# Keywords

- Hypothetical Judgments: an
entailmentbetween one or more hypotheses and a conclusion.Entailmenthas 2 notions:

derivabilityadmissibility- General Judgment: the universality or genericity of a judgment.
General Judgmenthas 2 forms:

genericparametric

# 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 derivableby $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`

- operator $\text{ap}$ with arity

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$.