2
$\begingroup$

Consider a set B (of binary strings) given by the introduction rules: \begin{equation} \frac{}{\epsilon :B} \quad \frac{a:B}{s_{0}(a):B} \quad \frac{a:B}{s_{1}(a):B}\end{equation}

\begin{equation} \frac{}{\epsilon=\epsilon:B} \quad \frac{a=c:B}{s_{0}(a)=s_{0}(c):B} \quad \frac{a=c:B}{s_{1}(a)=s_{1}(c):B}\end{equation}

Find elimination and computation rules corresponding to these introduction rules.

I have worked out a proposed solution that I would be very happy if anyone could be as so kind as to verify. Cheers!

Proposed Solution

Just as in natural deduction, the elimination rule can be thought of as essentially determined by the introduction rule. More specifically, the elimination rule shows how to define a function on the set in terms of the canonical elements, by introducing an elimination operator. The computation rule fixes the relation between the introduction and elimination rule. Thus, I am lead to believe that the following expressions form the B-elimination rules.

\begin{equation} \frac{z:B \vdash C(z) \quad \text{set} \quad \vdash c:B \quad \vdash d:C(\epsilon) \quad x:B,y:C(x) \vdash e(x,y):C(S_{1}(x))}{\vdash R(c,d,(x,y)e(x,y):C(c)} \tag{1}\end{equation}

\begin{equation} \frac{z:B \vdash C(z) \quad \text{set} \quad \vdash f:B \quad \vdash d:C(\epsilon) \quad x:B,y:C(x) \vdash e(x,y):C(S_{2}(x))}{\vdash R(f,d,(x,y)e(x,y):C(f)} \tag{2} \end{equation}

\begin{equation} \frac{z:B \vdash C(z) \text{set} \quad \vdash c=c':B \quad \vdash d=d':C(\epsilon) \quad x:B,y:C(x) \vdash e(x,y)=e'(x,y):C(S_{0}(x))}{\vdash R(c,d,(x,y)e(x,y))=R(c',d',(x,y)e'(x,y)):C(c)} \tag{3} \end{equation}

Here, that is (1), $R(c,d,(x,y)e(x,y))$ is a method which first computes $c$ to canonical form, which is either $d:C(\epsilon)$ or $e(x,y):C(S_{1}(x))$ with $x:B,y:C(x)$. I choose not to write out (4) as it is so similar.

B-computation

Continuing on, I have the following suggestions for the B-computational rules:

\begin{equation} \frac{z:B \vdash C(z) \quad \text{set} \quad \vdash d:C(\epsilon) \quad x:B,y:C(x) \vdash e(x,y):C(S_{0}(x))}{\vdash R(\epsilon,d,(x,y)e(x,y))=d:C(\epsilon)} \tag{1a}\end{equation}

\begin{equation} \frac{z:B \vdash C(z) \quad \text{set} \quad \vdash k:C(\epsilon) \quad x:B,y:C(x) \vdash e(x,y):C(S_{1}(x))}{\vdash R(\epsilon,k,(x,y)e(x,y))=k:C(\epsilon)} \tag{2a}\end{equation}

\begin{equation} \frac{z:B \vdash C(z) \text{set} \quad \vdash a:B \quad \vdash d:C(\epsilon) \quad x:B,y:C(x) \vdash e(x,y):C(S_{0}(x))}{\vdash R(S(a),d,(x,y)e(x,y))=e(a,R(a,d,(x,y)e(x,y))):C(S_{0}(a))} \tag{3a} \end{equation}

$\endgroup$

1 Answer 1

0
$\begingroup$

Your proposed solution has some problems: it seems you are a bit confused by $s_0$ and $s_1$. I'd like to explain in words what is wrong, but I think in this case it'll be clearer if I just write a correct elimination rule instead.

You should have only one elimination rule, that is the following:

$$ \frac{\vdash c : B \quad z : B \vdash C(z)\;\text{set} \quad \vdash d : C(\epsilon) \quad x: B,\, y: C(x)\vdash e(x, y) : C(s_0(x)) \quad x: B,\, y: C(x) \vdash f(x, y) : C(s_1(x))}{R(c, d, e, f) : C(c)}$$

plus of course the usual rule for equality. Then the computation rules should be:

$$ \frac{z : B \vdash C(z)\;\text{set} \quad \vdash d : C(\epsilon) \quad x: B,\, y: C(x)\vdash e(x, y) : C(s_0(x)) \quad x: B,\, y: C(x) \vdash f(x, y) : C(s_1(x))}{R(\epsilon, d, e, f) = d : C(\epsilon)}$$ $$ \frac{\vdash x : B \quad z : B \vdash C(z)\;\text{set} \quad \vdash d : C(\epsilon) \quad x: B,\, y: C(x)\vdash e(x, y) : C(s_0(x)) \quad x: B,\, y: C(x) \vdash f(x, y) : C(s_1(x))}{R(s_0(x), d, e, f) = e(x, R(x, d, e, f)) : C(s_0(x))}$$ $$ \frac{\vdash x : B \quad z : B \vdash C(z)\;\text{set} \quad \vdash d : C(\epsilon) \quad x: B,\, y: C(x)\vdash e(x, y) : C(s_0(x)) \quad x: B,\, y: C(x) \vdash f(x, y) : C(s_1(x))}{R(s_1(x), d, e, f) = f(x, R(x, d, e, f)) : C(s_1(x))}$$

Can you see the difference between your version and mine? Notice that you should have a homogeneous way to treat every term of type $B$. Since every term reduces to a canonical term, the recursive principle should know what to do when its first argument is $\epsilon$, $s_0(x)$ or $s_1(x)$.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .