<p>I have a question about proof by induction in the domain of session types. Let's assume we have the following lemma:</p>
<p><span class="math-container">$$
\text{Let}~ \Gamma \vdash P : T. ~~\text{If } P = \mu X. 
Q ~~\text{then}~~ \Gamma, X:T \vdash Q: T
$$</span></p>
<p>Now, I want to prove it by induction. I am quite familiar with the concept of &quot;proof by induction&quot; in maths but when I try to apply it to the area of <span class="math-container">$\pi$</span>-calculus or session types, I don't quite understand how to do it. For example, in the above lemma:</p>
<ol>
<li>What would be the base case?</li>
<li>What is the induction hypothesis?</li>
</ol>

CC BY-SA 4.0
2022-01-02T13:19:55.097Z
This question is more appropriate for
[cs.stackexchange.com](https://cs.stackexchange.com/).
Martin Berger
CC BY-SA 4.0
2022-01-02T13:20:51.500Z
Proving things about types, whether for process calculi or sequential
languages, often uses structural induction (on programs) or, more
frequently, induction on the typing derivation, which exploits a
subformula property of typing rules: in order to show that a composite
program $P = f(P_1, ..., P_n)$ has type $t$, you typically have to
establish that each $P_i$ has a specific type $t_i$. Hence the
derivation of each type $t_i$ is shorter than the derivation of
$t$ for $P$, which allows to apply induction.
Martin Berger
CC BY-SA 4.0
2022-01-02T13:21:54.410Z
We
cannot tell you what induction hypothesis you have to use, since if
the induction hypothesis was obvious, mathematics would be trivial. A
good starting point is to use the theorem you want to prove as IH, but
that's rarely strong enough. For example session types are strongly based on duality between input and output, so your IH typically needs to state something about both. Note also that if you want to prove
something about non-terminating processes, other forms of induction
might be needed, for example coinduction.
Martin Berger
CC BY-SA 4.0
2022-01-02T13:22:27.107Z
The relationship between the forms of induction used in programming language research (except coinduction) is
explained in great detail in Chapter 3 of Winskel's nice book *The                                                                                                                                                  
Formal Semantics of Programming Languages: An Introduction*.
Martin Berger
CC BY-SA 4.0
2022-01-03T18:40:33.847Z
@MartinBerger Thank you very much. Very helpful tips and explanations!
Coder
<type-systems><proofs><pi-calculus>
A fundamental question about the proof by induction in session types
Coder
# A fundamental question about the proof by induction in session types

(Asked by: username_0 on 2021-12-31)

I have a question about proof by induction in the domain of session types. Let's assume we have the following lemma:

$$
\text{Let}~ \Gamma \vdash P : T. ~~\text{If } P = \mu X.
Q ~~\text{then}~~ \Gamma, X:T \vdash Q: T
$$

Now, I want to prove it by induction. I am quite familiar with the concept of "proof by induction" in maths but when I try to apply it to the area of $\pi$-calculus or session types, I don't quite understand how to do it. For example, in the above lemma:

1. What would be the base case?
2. What is the induction hypothesis?

**Tags:** type-systems, proofs, pi-calculus
> **Comments:**
> **username_1**: This question is more appropriate for [cs.stackexchange.com](https://cs.stackexchange.com/).  
> **username_1**: Proving things about types, whether for process calculi or sequential languages, often uses structural induction (on programs) or, more frequently, induction on the typing derivation, which exploits a subformula property of typing rules: in order to show that a composite program $P = f(P_1, ..., P_n)$ has type $t$, you typically have to establish that each $P_i$ has a specific type $t_i$. Hence the derivation of each type $t_i$ is shorter than the derivation of $t$ for $P$, which allows to apply induction.  
> **username_1**: We cannot tell you what induction hypothesis you have to use, since if the induction hypothesis was obvious, mathematics would be trivial. A good starting point is to use the theorem you want to prove as IH, but that's rarely strong enough. For example session types are strongly based on duality between input and output, so your IH typically needs to state something about both. Note also that if you want to prove something about non-terminating processes, other forms of induction might be needed, for example coinduction.  
> **username_1**: The relationship between the forms of induction used in programming language research (except coinduction) is explained in great detail in Chapter 3 of Winskel's nice book *The                                                                                                                                                   Formal Semantics of Programming Languages: An Introduction*.  
> **username_0**: @MartinBerger Thank you very much. Very helpful tips and explanations!  

---

## 0 answers

