0
$\begingroup$

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?
$\endgroup$
5
  • $\begingroup$ This question is more appropriate for cs.stackexchange.com. $\endgroup$ Jan 2 at 13:19
  • $\begingroup$ 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. $\endgroup$ Jan 2 at 13:20
  • $\begingroup$ 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. $\endgroup$ Jan 2 at 13:21
  • $\begingroup$ 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. $\endgroup$ Jan 2 at 13:22
  • $\begingroup$ @MartinBerger Thank you very much. Very helpful tips and explanations! $\endgroup$
    – Coder
    Jan 3 at 18:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.