compiler

Inductive Definitions Introduction

ref:Lecture Notes on Inductive Definitions

Judgements (prediction, assertion, …)

Examples:

$$\begin{array}{ll}n\text{even}& n\text{is an even number}\\ \text{type}(\tau )& \tau \text{is a type}\\ e:\tau & \text{expression}e\text{has type }\tau \\ \text{live}(l,x)& \text{variable }x\text{ is live at line }l\end{array}$$

Inductive Definitions

Examples

• Natural number
  1. nat(0)
  2. nat(n) ⇒ nat(n+1)
• Relation $n\le m$ in natual number
  1. leq(0, 0)
  2. leq(n, m) ⇒ leq(n+1, m+1)
  3. leq(n, m) ⇒ leq(n, m+1)

Inference Rules

Assume a given inductive definition with a rules of the form:

$$P_1\text{ and }\cdots \text{ and }{P}_n\Rightarrow P$$

From now on, we will write such rule as:

$$\frac{\begin{array}{l}{P}_1\\ \cdots \\ P_n\end{array}}{P}(Rul{e}_1)$$

For example, the judgement nat(n) is defined by the following rules:

\begin{array}{}\\ \hline \text{nat}(0)\end{array}N_1& \begin{array}{}\text{nat}(n)\\ \hline \text{nat}(n+1)\end{array}N_1 \end{array}

The judgement leq(n, m) is defined by the following rules:

\begin{array}{}\\ \hline \text{leq}(0, 0)\end{array}L_1 & \begin{array}{}\text{leq}(n, m) \\ \hline \text{leq}(n+1, m+1)\end{array}L_2 & \begin{array}{}\text{leq}(n, m) \\ \hline \text{leq}(n, m+1)\end{array}L_3 & \end{array}$$ ## Derivations ![[Pasted image.png]]