diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index a569f6b..3dbd8f9 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -230,6 +230,7 @@ "lastOpenFiles": [ "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/13 - CCS cose varie.md", + "Pasted image 20250415090109.png", "Concurrent Systems/notes/12 - Calculus of communicating system.md", "Pasted image 20250415082906.png", "Concurrent Systems/notes/11 - LTSs and Bisimulation.md", @@ -242,7 +243,6 @@ "Concurrent Systems/notes/images/Pasted image 20250414152247.png", "Concurrent Systems/notes/images/Pasted image 20250414152234.png", "Concurrent Systems/notes/images/Pasted image 20250414152221.png", - "Concurrent Systems/notes/images/Pasted image 20250414104010.png", "HCIW/notes/3 - Beacons.md", "HCIW/slides/Zooming interfaces.pdf", "HCIW/slides/Gestural interaction.pdf", diff --git a/Concurrent Systems/notes/13 - CCS cose varie.md b/Concurrent Systems/notes/13 - CCS cose varie.md index 8ba455a..7d7e55c 100644 --- a/Concurrent Systems/notes/13 - CCS cose varie.md +++ b/Concurrent Systems/notes/13 - CCS cose varie.md @@ -47,5 +47,12 @@ Let's go! One of the main aims of an equivalence notion between processes is to make equational reasonings of the kind: “if P and Q are equivalent, then they can be interchangeably used in any execution context”. This feature on an equivalence makes it a *congruence* -Not all equivalences are necessarily congruences (even though most of them are -To properly define a congruence, we first need to define an execution context, and then what it means to run a process in a context. Intuitively: \ No newline at end of file +Not all equivalences are necessarily congruences (even though most of them are). +To properly define a congruence, we first need to define an execution context, and then what it means to run a process in a context. Intuitively: +![200](../../Pasted%20image%2020250415090109.png) + +where C is a context (i.e., a process with a hole ☐), P is a process, and $C[P]$ denotes filling the hole with P + +Example: $$if \space C = (☐ | Q) \textbackslash a, \space then \space C[P] = (P | Q) \textbackslash a$$ +The set C of CCS contexts is given by the following grammar: +$$C ::= ☐ \space | \space C|P \space | $$ \ No newline at end of file diff --git a/Pasted image 20250415090109.png b/Pasted image 20250415090109.png new file mode 100644 index 0000000..805800e Binary files /dev/null and b/Pasted image 20250415090109.png differ