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}