| # Notation |
|
|
| Overview of the notation for common concepts. |
|
|
| ## Equivalences |
| - Alpha equivalence: `m =α n` |
| - Bisimilarity: `p ~[lts] q` (`p` is bisimilar to `q` in the LTS `lts`) |
|
|
| ## Operational semantics |
|
|
| ### Option A |
| This option uses an extra arrow head to denote reflexive and transitive closure. |
|
|
| When there is only 'one' semantics: |
| - Reduction: `m → n`. |
| - Multi-step reduction (possibly zero): `m ↠ n`. |
| - Transition: `p [μ]→ q`, where `μ` is a transition label. |
| - Multi-step transition (possibly zero): `p [μs]↠ q`, where `μs` is a list of transition labels. |
| - Saturated transitions: `p [μ]⇒ q`. |
| - Multi-step saturated transitions: `p [μs]➾ q`. |
|
|
| When there are 'alternative' semantics, we suffix the arrow with the name of the transition relation or LTS under use. For example `m →[cbv] n` means that there is a reduction from `m` to `n` under the `cbv` reduction relation. |
| Another example: transitions look like `p [μ]→[late] q`, where `late` is an `LTS`. |
|
|
| ### Option B |
|
|
| As Option A, but uses `*` to denote reflexive and transitive closure. |
| - Multi-step reduction (possibly zero): `m →* n`. |
| - Multi-step transition (possibly zero): `p [μs]→* q`, where `μs` is a list of transition labels. |
| - Saturated transitions: `p [μ]⇒ q`. |
| - Multi-step saturated transitions: `p [μs]⇒* q`. |
|
|
| ### Option C |
| Like Option A, but with triangle heads (`⭢`) to distinguish arrows from the usual implication in Lean (`→`). E.g., `(m ⭢ n) → (n ⭢ s) → (m ⯮ s)`. |
|
|
| When there is only 'one' semantics: |
| - Reduction: `m ⭢ n`. |
| - Multi-step reduction (possibly zero): `m ⯮ n`. |
| - Transition: `p μ⭢ q`, where `μ` is a transition label. |
| - Multi-step transition (possibly zero): `p [μs]⯮ q`, where `μs` is a list of transition labels. |
| - Saturated transitions: `p μ⇒ q`. |
| - Multi-step saturated transitions: `p μs➾ q`. |
|
|
| When there are 'alternative' semantics, we suffix the arrow with the name of the transition relation or LTS under use. For example `m ⭢cbv n` means that there is a reduction from `m` to `n` under the `cbv` reduction relation. |
| Another example: transitions look like `p μ⭢late q`, where `late` is an `LTS`. |
|
|
