Evgenii Akentev
·
2019-01-18
Theorems.lagda
1\chapter{Proofs of properties}
2
3\if{False}
4\begin{code}
5-- Imports
6{-# OPTIONS --allow-unsolved-metas #-}
7open import Prelude
8
9open import Syntax
10open import Typesystem
11open import Typingrules
12open import Semantics
13\end{code}
14\fi
15
16According to the Curry-Howard isomorphism~\cite{Sorensen}, types of the programs are propositions and terms are proofs. For example, the type $ A \rightarrow B $ corresponds to the implication from $ A $ to $ B $, and, at the same time, such function $ f $ that takes an element of type $ A $ and returns an element of type $ B $ will be a proof of this theorem.
17
18To demonstrate the correctness of the typing rules given before, I provide the proof of the lemma called "Structural Congruence for Behaviours"~\cite{nielsen2013type,engelfriet} and the proofs of particular cases of "Type preservation of behaviours".
19
20\section{Structural Congruence for Behaviours}\label{sec:strcongr}
21
22Since Jolie~\cite{montesi2010jolie} is based on $\pi$-calculus~\cite{Milner1999}, it should have the same properties. $\pi$-calculus has the following structural congruence rules, which apply at behaviour layer in Jolie:
23
24$$ (B_1\ |\ B_2)\ |\ B_3 \equiv B_1\ |\ (B_2\ |\ B_3) $$
25$$ 0\ ;\ B\ \equiv B $$
26$$ B_1\ |\ B_2 \equiv B_2\ |\ B_1 $$
27$$ B\ |\ 0 \equiv B $$
28
29Two structural congruent behaviours are typable with respect to the same environment and they make the same updates to the environment during type checking:
30
31\newpage
32
33\begin{lemma} Structural Congruence for Behaviours
34
35\begin{center}
36\textit{Let} $ \Gamma \vdash B_1 \rhd \Gamma' $ \\
37\textit{If} $ B_1 \equiv B_2 $ \\
38\textit{then} $ \Gamma \vdash B_2 \rhd \Gamma' $
39\end{center}
40
41\end{lemma}
42
43\begin{proof}
44The proof is the case analysis of all possible behaviours $ B_1 $ and $ B_2 $ according to the rules provided above.
45
46\begin{itemize}
47
48\item \textit{Case} $ B_1 \equiv B_2 $
49
50The proof is done by Agda's pattern matching mechanism. Since \AgdaDatatype{b_1 ≡ b_2}, Agda replaces $b_1$ in the term t to $b_2$.
51
52\begin{code}
53struct-cong-b₁≡b₂ : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour}
54 → Γ ⊢B b₁ ▹ Γ₁
55 → b₁ ≡ b₂
56 → Γ ⊢B b₂ ▹ Γ₁
57struct-cong-b₁≡b₂ t refl = t
58\end{code}
59
60\item \textit{Case} $ 0; B \equiv B $
61
62This proof is done by decomposing the term by pattern matching.
63
64\begin{code}
65struct-cong-nil∶b→b : {Γ Γ₁ : Context} {b : Behaviour}
66 → Γ ⊢B nil ∶ b ▹ Γ₁
67 → Γ ⊢B b ▹ Γ₁
68struct-cong-nil∶b→b (t-seq t-nil x) = x
69\end{code}
70
71\item \textit{Case} $ B \equiv 0 ; B $
72
73In this proof, instead of decomposition, I construct the resulting term by using $x$.
74
75\begin{code}
76struct-cong-b→nil∶b : {Γ Γ₁ : Context} {b : Behaviour}
77 → Γ ⊢B b ▹ Γ₁
78 → Γ ⊢B nil ∶ b ▹ Γ₁
79struct-cong-b→nil∶b x = t-seq t-nil x
80\end{code}
81
82\item \textit{Case} $ B \parallel 0 \equiv B $
83\begin{code}
84struct-cong-b∥nil→b : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b : Behaviour}
85 → & Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ & Γ₁' Γ₂'
86 → Γ₁ ⊢B b ▹ Γ₁'
87struct-cong-b∥nil→b (t-par x _) = x
88\end{code}
89
90\item \textit{Case} $ B \equiv B \parallel 0 $
91
92\begin{code}
93struct-cong-b→b∥nil : {Γ₁ Γ₂ Γ₃ : Context} {b : Behaviour}
94 → Γ₁ ⊢B b ▹ Γ₂
95 → & Γ₁ Γ₃ ⊢B (b ∥ nil) ▹ & Γ₂ Γ₃
96struct-cong-b→b∥nil x = t-par x t-nil
97\end{code}
98
99\item \textit{Case} $ B_1 \parallel B_2 \equiv B_2 \parallel B_1 $
100
101In this case, I just swap terms $t_1$ and $t_2$.
102
103\begin{code}
104struct-cong-par-comm : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}
105 → & Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ & Γ₁' Γ₂'
106 → & Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ & Γ₂' Γ₁'
107struct-cong-par-comm (t-par t₁ t₂) = t-par t₂ t₁
108\end{code}
109
110\item \textit{Case} $ (B_1 \parallel B_2) \parallel B_3 \equiv B_1 \parallel (B_2 \parallel B_3) $
111
112The last proof is the most complex one, but it's just a swapping of terms too.
113
114\begin{code}
115struct-cong-par-assoc : {Γ₁ Γ₂ Γ₃ Γ₁' Γ₂' Γ₃' : Context} {b₁ b₂ b₃ : Behaviour}
116 → & (& Γ₁ Γ₂) Γ₃ ⊢B (b₁ ∥ b₂) ∥ b₃ ▹ & (& Γ₁' Γ₂') Γ₃'
117 → & Γ₁ (& Γ₂ Γ₃) ⊢B b₁ ∥ (b₂ ∥ b₃) ▹ & Γ₁' (& Γ₂' Γ₃')
118struct-cong-par-assoc (t-par (t-par t1 t2) t3) = t-par t1 (t-par t2 t3)
119\end{code}
120
121The proof for $ B_1 \parallel (B_2 \parallel B_3) \equiv (B_1 \parallel B_2) \parallel B_3 $ is similar.
122
123\end{itemize}
124\end{proof}
125
126\section{Type preservation for behaviours}
127
128Type preservation is a property such that if a well-typed behaviour takes a transition then the resulting behaviour is well-typed too. Since the typing rule (or judgement) for behaviours is a Hoare triple which consists of an initial environment, a behaviour and a resulting environment, type preservation property requires that the resulting environment for a behaviour after a transition is equal to the resulting environment for the behaviour before the transition.
129
130At first, I need to define what a transition or a side effect is. The type preservation property takes place when a behaviour takes a transition. Actions are performed during the transitions, therefore the transition function is defined with respect to the performed action.
131
132Let $B$ and $B'$ be two behaviours and $\eta$ is a label defined before in chapter 4. Suppose that there is a transition $ B \xrightarrow{\eta} B' $, $B$ is typed with respect to $\Gamma$, $B'$ is typed with respect to $\Gamma'$, then the relation between $\Gamma$ and $\Gamma'$ is defined as a side effect of $\eta$. It is described as the type \AgdaDatatype{\_↦⟨\_⟩\_}:
133
134\begin{code}
135data _↦⟨_⟩_ : Context → Label → Context → Set where
136\end{code}
137
138The first constructor of that type is \AgdaInductiveConstructor{s-nil}. It shows that nothing is done to the context since the label is \AgdaInductiveConstructor{lb-nil}.
139
140\begin{code}
141 s-nil : {Γ : Context}
142 → Γ ↦⟨ lb-nil ⟩ Γ
143\end{code}
144
145The same thing is with \AgdaInductiveConstructor{lb-read} label. It has no any side effects.
146
147\begin{code}
148 s-read : {Γ : Context} {t : State}
149 → Γ ↦⟨ lb-read t ⟩ Γ
150\end{code}
151
152The \AgdaInductiveConstructor{s-assign} constructor is for the assignment behaviour when the variable is already in the context. It does not effect the context.
153
154\begin{code}
155 s-assign : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
156 → Γ ⊢ₑ e ∶ Tₑ
157 → x ∶ Tₓ ∈ Γ
158 → Tₓ ≡ Tₑ
159 → Γ ↦⟨ lb-assign x e ⟩ Γ
160\end{code}
161
162The next three constructors are cases of adding a variable in the context for the assignment behaviour. They are similar to typing rules for the assignment behaviour. The first one is for simple context and the two last are for a disjoint union context. It's important to notice that the label is \AgdaInductiveConstructor{lb-assign} $x$ $e$. It depends on the variable $x$ and the expression $e$.
163
164\begin{code}
165 s-assign-upd : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
166 → ⋆ Γ ⊢ₑ e ∶ Tₑ
167 → ¬ (x ∶ Tₓ ∈ ⋆ Γ)
168 → ⋆ Γ ↦⟨ lb-assign x e ⟩ ⋆ ((x ∶ Tₓ) ∷ Γ)
169
170 s-assign-upd-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable}
171 {e : Expr} {Tₓ Tₑ : Type}
172 → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ
173 → ¬ (x ∶ Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
174 → & (⋆ Γ) (⋆ Γ₁) ↦⟨ lb-assign x e ⟩ & (⋆ ((x ∶ Tₓ) ∷ Γ)) (⋆ Γ₁)
175
176 s-assign-upd-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {x : Variable}
177 {e : Expr} {Tₓ Tₑ : Type}
178 → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ
179 → ¬ (x ∶ Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
180 → & (⋆ Γ) (⋆ Γ₁) ↦⟨ lb-assign x e ⟩ & (⋆ Γ) (⋆ ((x ∶ Tₓ) ∷ Γ₁))
181\end{code}
182
183
184Assume that $B$ is a well-typed behaviour typed with respect to an environment $\Gamma$ and $\Gamma'$ is a resulting environment. Suppose that there is a behaviour $B'$ such that $ B \xrightarrow{\eta} B' $. Then there is an environment $\Gamma''$ which is an update of $\Gamma$, caused by as a result of side effect with label $\eta$ and $ B'$ is typed with respect to the environments $\Gamma''$ and $\Gamma'$:
185
186\begin{theorem} Type Preservation for Behaviours
187\begin{center}
188\textit{If} $ \Gamma \vdash _{B} B \rhd \Gamma' $ \\
189\textit{and} $ B \xrightarrow{\eta} B' $ \\
190\textit{then} $ \Gamma'' \vdash _{B} B' \rhd \Gamma' $ \\
191\textit{where} $ \Gamma'' =$ \textit{sideEffect} $ (\eta,\ \Gamma) $
192\end{center}
193\end{theorem}
194
195
196\begin{proof} The proofs of simple cases are a case analysis of a typing rule, a side effect and a semantic rule. The type is almost the same as the theorem, but there is one difference. In the theorem, $\Gamma''$ may be replaced with the \textit{sideEffect} $ (\eta,\ \Gamma) $, but in the type of \AgdaDatatype{type-preservation}, I use a side effect as an additional argument.
197
198\begin{code}
199type-preservation : {Γ Γ′ Γ′′ : Context} {b b′ : Behaviour} {η : Label}
200 → Γ ⊢B b ▹ Γ′
201 → b ↝ b′ ∶ η
202 → Γ ↦⟨ η ⟩ Γ′′
203 → Γ′′ ⊢B b′ ▹ Γ′
204type-preservation t-nil b-nil s-nil = t-nil
205type-preservation (t-if x t t₁) (b-if-then _) s-read = t
206type-preservation (t-if x t t₁) (b-if-else _) s-read = t₁
207type-preservation (t-assign-exists _ _ _) (b-assign) (s-assign _ _ _) = t-nil
208type-preservation = {!!}
209\end{code}
210
211The last line is a type hole. It means that the proof is not complete, not all cases of arguments are covered. Other cases are intended for the future research.
212
213\end{proof}