|
5 | 5 | \chapter{Derived Requirements Summary}\label{derived summary} |
6 | 6 |
|
7 | 7 | \index{$\vdash$} |
8 | | -\IndexStep{GenSig} |
9 | | -\IndexStep{ReqSig} |
10 | | -\IndexStep{AssocType} |
11 | | -\IndexStep{Conf} |
12 | | -\IndexStep{Equiv} |
13 | | -\IndexStep{Same} |
14 | | -\IndexStep{Member} |
15 | | -\IndexStep{Concrete} |
16 | 8 |
|
| 9 | +Let $G$ be a \index{generic signature!summary}generic signature. We generate the theory of~$G$ by repeated application of inference rules, starting from a finite set of elementary statements. A derivation proves that some element belongs to this set by giving a list of derivation steps where the assumptions in each step are conclusions of previous steps. Nomenclature: |
| 10 | +\begin{center} |
| 11 | +\begin{tabular}{ll} |
| 12 | +\toprule |
| 13 | +\textbf{Symbol}&\textbf{Description}\\ |
| 14 | +\midrule |
| 15 | +\texttt{T}, \texttt{U}, and \texttt{V}&\index{type parameter!summary}type parameters\\ |
| 16 | +\texttt{Self.U} and \texttt{Self.V}&type parameters rooted in the \index{protocol Self type!summary}protocol \texttt{Self} type\\ |
| 17 | +\texttt{X}&a concrete type\\ |
| 18 | +\texttt{C}&a concrete \index{class type!summary}class type\\ |
| 19 | +$\Xprime$ and $\Cprime$&obtained from \texttt{X} and \texttt{C} by replacing \texttt{Self} with \texttt{T}\\ |
| 20 | +\texttt{P} and \texttt{Q}&protocols\\ |
| 21 | +\texttt{A}&the name of an \index{associated type declaration!summary}associated type of \texttt{P}\\ |
| 22 | +\texttt{[P]A}&an associated type declaration of \texttt{P}\\ |
| 23 | +\texttt{T.[P]A} and \texttt{T.A}&\index{bound dependent member type!summary}bound and \index{unbound dependent member type!summary}unbound dependent member type\\ |
| 24 | +$\ConfReq{T}{P}$&a \index{conformance requirement!summary}conformance requirement\\ |
| 25 | +$\SameReq{T}{U}$&a \index{same-type requirement!summary}same-type requirement between type parameters\\ |
| 26 | +$\SameReq{T}{X}$&a concrete same-type requirement\\ |
| 27 | +$\ConfReq{T}{C}$&a \index{superclass requirement!summary}superclass requirement\\ |
| 28 | +$\ConfReq{T}{AnyObject}$&a \index{layout requirement!summary}layout requirement\\ |
| 29 | +$\ConfReq{Self.U}{Q}_\texttt{P}$&an \index{associated requirement!summary}associated requirement of protocol \texttt{P}\\ |
| 30 | +\bottomrule |
| 31 | +\end{tabular} |
| 32 | +\end{center} |
| 33 | +See \index{derived requirement!summary}\index{valid type parameter!summary}\SecRef{derived req} and \SecRef{type params} for details. |
| 34 | + |
| 35 | +\index{elementary derivation step!summary}\paragraph{Elementary statements.} |
| 36 | +For \IndexStepTwo{Generic}{summary}each generic parameter \ttgp{d}{i} of~$G$: |
| 37 | +\begin{gather*} |
| 38 | +\GenericStepDef |
| 39 | +\end{gather*} |
| 40 | +For \IndexStepTwo{Conf}{summary}\IndexStepTwo{Same}{summary}\IndexStepTwo{Concrete}{summary}\IndexStepTwo{Super}{summary}\IndexStepTwo{Layout}{summary}each explicit requirement of~$G$ by \index{requirement kind!summary}kind: |
| 41 | +\begin{gather*} |
| 42 | +\ConfStepDef\\ |
| 43 | +\SameStepDef\\ |
| 44 | +\ConcreteStepDef\\ |
| 45 | +\SuperStepDef\\ |
| 46 | +\LayoutStepDef |
| 47 | +\end{gather*} |
| 48 | + |
| 49 | +\index{requirement signature!summary} |
| 50 | +\paragraph{Requirement signatures.} |
| 51 | +Assume $G\vdash\ConfReq{T}{P}$. For \IndexStepTwo{AssocName}{summary}\IndexStepTwo{AssocDecl}{summary}\IndexStepTwo{AssocBind}{summary}each associated type~\texttt{A} of~\texttt{P}: |
| 52 | +\begin{gather*} |
| 53 | +\AssocNameStepDef\\ |
| 54 | +\AssocDeclStepDef\\ |
| 55 | +\AssocBindStepDef |
| 56 | +\end{gather*} |
| 57 | +For each \IndexStepTwo{AssocConf}{summary}\IndexStepTwo{AssocSame}{summary}\IndexStepTwo{AssocConcrete}{summary}\IndexStepTwo{AssocSuper}{summary}\IndexStepTwo{AssocLayout}{summary}associated requirement of~\texttt{P} by kind: |
| 58 | +\begin{gather*} |
| 59 | +\AssocConfStepDef\\ |
| 60 | +\AssocSameStepDef\\ |
| 61 | +\AssocConcreteStepDef\\ |
| 62 | +\AssocSuperStepDef\\ |
| 63 | +\AssocLayoutStepDef |
| 64 | +\end{gather*} |
| 65 | + |
| 66 | +\paragraph{Equivalence.} |
| 67 | +Same-type requirements \IndexStepTwo{Reflex}{summary}\IndexStepTwo{Sym}{summary}\IndexStepTwo{Trans}{summary}generate an equivalence relation: |
| 68 | +\begin{gather*} |
| 69 | +\ReflexStepDef\\ |
| 70 | +\SymStepDef\\ |
| 71 | +\TransStepDef |
| 72 | +\end{gather*} |
| 73 | + |
| 74 | +\paragraph{Compatibility.} |
| 75 | +A derived conformance, superclass or layout requirement \IndexStepTwo{SameConf}{summary}\IndexStepTwo{SameSuper}{summary}\IndexStepTwo{SameLayout}{summary}\IndexStepTwo{SameName}{summary}\IndexStepTwo{SameDecl}{summary}applies to all type parameters in an equivalence class: |
| 76 | +\begin{gather*} |
| 77 | +\SameConfStepDef\\ |
| 78 | +\SameConcreteStepDef\\ |
| 79 | +\SameSuperStepDef\\ |
| 80 | +\SameLayoutStepDef |
| 81 | +\end{gather*} |
| 82 | +If two type parameters are equivalent, so are \IndexStepTwo{SameName}{summary}\IndexStepTwo{SameDecl}{summary}all corresponding member types: |
17 | 83 | \begin{gather*} |
18 | | -\vdash\ConfReq{T}{P}\tag{\textsc{GenSig}}\\ |
19 | | -\vdash\ConfReq{T}{C}\\ |
20 | | -\vdash\ConfReq{T}{AnyObject}\\ |
21 | | -\vdash\FormalReq{T == U}\\[\medskipamount] |
22 | | -\ConfReq{T}{P}\vdash\texttt{T.A}\tag{\textsc{AssocType}}\\ |
23 | | -\ConfReq{T}{P}\vdash\texttt{T.[P]A}\\ |
24 | | -\ConfReq{T}{P}\vdash\FormalReq{T.[P]A == T.A}\\[\medskipamount] |
25 | | -\vdash\ConfReq{Self.U}{Q}_\texttt{P}\tag{\textsc{ReqSig}}\\ |
26 | | -\vdash\ConfReq{Self.U}{C}_\texttt{P}\\ |
27 | | -\vdash\ConfReq{Self.U}{AnyObject}_\texttt{P}\\ |
28 | | -\vdash\FormalReq{Self.U == Self.V}_\texttt{P}\\[\medskipamount] |
29 | | -\ConfReq{T}{P},\,\ConfReq{Self.U}{Q}\vdash\ConfReq{T.U}{Q}\tag{\textsc{Conf}}\\ |
30 | | -\ConfReq{T}{P},\,\ConfReq{Self.U}{C}\vdash\ConfReq{T.U}{C}\\ |
31 | | -\ConfReq{T}{P},\,\ConfReq{Self.U}{AnyObject}\vdash\ConfReq{T.U}{AnyObject}\\ |
32 | | -\ConfReq{T}{P},\,\FormalReq{Self.U == Self.V}\vdash\FormalReq{T.U == T.V}\\[\medskipamount] |
33 | | -\texttt{T}\vdash\FormalReq{T == T}\tag{\textsc{Equiv}}\\ |
34 | | -\FormalReq{T == U}\vdash\FormalReq{U == T}\\ |
35 | | -\FormalReq{T == U},\,\FormalReq{U == V}\vdash\FormalReq{T == V}\\[\medskipamount] |
36 | | -\ConfReq{U}{P},\,\FormalReq{T == U}\vdash\ConfReq{T}{P}\tag{\textsc{Same}}\\ |
37 | | -\ConfReq{U}{C},\,\FormalReq{T == U}\vdash\ConfReq{T}{C}\\ |
38 | | -\ConfReq{U}{AnyObject},\,\FormalReq{T == U}\vdash\ConfReq{T}{AnyObject}\\[\medskipamount] |
39 | | -\ConfReq{U}{P},\,\FormalReq{T == U}\vdash\FormalReq{T.A == U.A}\tag{\textsc{Member}}\\ |
40 | | -\ConfReq{U}{P},\,\FormalReq{T == U}\vdash\FormalReq{T.[P]A == U.[P]A}\\[\medskipamount] |
41 | | -\FormalReq{T == U}\vdash\FormalReq{G<T> == G<U>}\qquad\mbox{(arbitrary type constructor \texttt{G<>})}\tag{\textsc{Concrete}}\\ |
42 | | -\FormalReq{G<T> == G<U>}\vdash\FormalReq{T == U}\qquad\mbox{(arbitrary type constructor \texttt{G<>})} |
| 84 | +\SameNameStepDef\\ |
| 85 | +\SameDeclStepDef |
43 | 86 | \end{gather*} |
44 | 87 |
|
45 | | -\end{document} |
| 88 | +\end{document} |
0 commit comments