1-9 Set Theory (II):Relations 魏恒峰 hfwei@nju.edu.cn 2019年12月03日 4口·￥①，43，t夏，里Q0 Hengfeng Wei (hfweiinju.edu.cn)1-9 Set Theory (II):Relations 2019年12月03日1/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1-9 Set Theory (II): Relations 魏恒峰 hfwei@nju.edu.cn 2019 年 12 月 03 日 Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 1 / 51
Set Theory Foundation A Branch of Math- of Math- ematics ematies (Loglc) (a,b) A→B N,R ) AxB RC AxB Hengfeng Wei (hfweixinju.edu.cn) 1-9 Set Theory (II):Relations 2019年12月03日2/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Set Theory A Branch of Mathematics N, R ℵ0 ω Foundation of Mathematics (+ Logic) (a, b) {} A × B R ⊆ A × B f : A → B Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 2 / 51
门店=种V方 DVx.2A 2 1E网门=程U为+三疗4a,,门 Figure 13.A selection of consitency axkomns over an execution [E,repl.obj,oper.rval;ro,vi, Auxiliary relations ameobj6f》←→cbe)=dbj门 LU有w1r4 Per-object (aka heopens-befure)order hbo [frof sameobi]Uvis]t Causality (aka happen-befure)oeder hb=[roUvis]+ =可国加=《者 a时imi EVENTUAL e∈E.(3 infiniely my∈E.ameobj(e,.fnA-e凸f》 THNA孩：ro Uvis is acyclic POCV (Per-Object Causal Visibility]:hbo C vis POCA (Per-Object Causal Arbimation):hhe C ar COCV (Crons-Ohject Causal Viibility::(hb n sameobj)C vis COCA (Cros-Object Causal Arbitralion:hb U ar is acyehe 0a0 Hengfeng Wei (hfwei&inju.edu.cn) 1-9 Set Theory (II):Relations 2019年12月03日 3/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 3 / 51
. 门=种 2w,4 rm 1E网门=程U为+三疗4a,,门 Figure 13.A selection of consitency axkomns over an execution [E,repl.obj,oper.rval;ro,vis, Auxiliary relations ameobj(e,f》←→cbe)=dbj门 LU有w1r4 Per-object (aka heopens-befure)order hbo [frof sameobi]Uvis]t Causality (aka happen-before)oeder hb=(roUvis]+ =可m加=长《青 EVENTUAL e∈E.(3 infiniely my∈E.ameobj(e,.fnA-e凸f》 THINA孩：ro Uvis is acyclic POCV (Per-Object Causal Visibility]:hbo C vis POCA (Per-Object Causal Arbimation):hhe C ar COCV (Cros-Ohject Causal Viibility):(hbn sameobj)C vis 2 COCA (Cros-Object Causal Arbitralion:hb U ar is acyehe Hengfeng Wei (hfwei&inju.edu.cn) 1-9 Set Theory (II):Relations 2019年12月03日 3/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 3 / 51
DON'T BE SCARED FOR CHILDREN BY WELL-LOVED AUTHORG B ARTISTB 4口·￥①，43，t夏，里Q0 Hengfeng Wei (hfweiinju.edu.cn)1-9 Set Theory (II):Relations 2019年12月03日4/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 4 / 51
I'm so excited. DON'T BE SCARED FOR CHILDREN BY WELL-LOVED AUTHORG B ARTISTB 4口·￥①，43，t夏，里Q0 Hengfeng Wei (hfweiinju.edu.cn)1-9 Set Theory (II):Relations 2019年12月03日4/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 4 / 51
Definition (Relations) A relation R from A to B is a subset of A x B: RCAXB 4口，1①，43，t夏，3080 Hengfeng Wei (hfweiinju.edu.cn)1-9 Set Theory (II):Relations 2019年12月03日5/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Definition (Relations) A relation R from A to B is a subset of A × B: R ⊆ A × B Definition (Cartesian Products) The Cartesian product A × B of A and B is defined as A × B ≜ {(a, b) | a ∈ A ∧ b ∈ B} Axiom (Ordered Pairs) (a, b) = (c, d) ⇐⇒ a = c ∧ b = d Q : Are you satisfied with the definitions above? Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 5 / 51
Definition (Relations) A relation R from A to B is a subset of A x B: RCAXB Definition (Cartesian Products) The Cartesian product A x B of A and B is defined as A×B≌{(a,b)|a∈A∧b∈B} 4口，1①，43，t夏，3080 Hengfeng Wei (hfweiinju.edu.cn)1-9 Set Theory (II):Relations 2019年12月03日5/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Definition (Relations) A relation R from A to B is a subset of A × B: R ⊆ A × B Definition (Cartesian Products) The Cartesian product A × B of A and B is defined as A × B ≜ {(a, b) | a ∈ A ∧ b ∈ B} Axiom (Ordered Pairs) (a, b) = (c, d) ⇐⇒ a = c ∧ b = d Q : Are you satisfied with the definitions above? Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 5 / 51
Definition (Relations) A relation R from A to B is a subset of A x B: RCAXB Definition(Cartesian Products) The Cartesian product A x B of A and B is defined as A×B≌{(a,b)|a∈AAb∈B} Axiom (Ordered Pairs) (a,b)=(c,d)→a=c∧b=d 4口，1①，43，t夏，3080 Hengfeng Wei (hfweixinju.edu.cn) 1-9 Set Theory (II):Relations 2019年12月03日5/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Definition (Relations) A relation R from A to B is a subset of A × B: R ⊆ A × B Definition (Cartesian Products) The Cartesian product A × B of A and B is defined as A × B ≜ {(a, b) | a ∈ A ∧ b ∈ B} Axiom (Ordered Pairs) (a, b) = (c, d) ⇐⇒ a = c ∧ b = d Q : Are you satisfied with the definitions above? Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 5 / 51
Definition (Relations) A relation R from A to B is a subset of A x B: RCAXB Definition(Cartesian Products) The Cartesian product A x B of A and B is defined as A×B≌{(a,b)|a∈AAb∈B} Axiom (Ordered Pairs) (a,b)=(c,d)→a=c∧b=d Q:Are you satisfied with the definitions above? 4口，￥①，43，t豆，30Q0 Hengfeng Wei (hfweiinju.edu.cn)1-9 Set Theory (II):Relations 2019年12月03日5/51
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Definition (Relations) A relation R from A to B is a subset of A × B: R ⊆ A × B Definition (Cartesian Products) The Cartesian product A × B of A and B is defined as A × B ≜ {(a, b) | a ∈ A ∧ b ∈ B} Axiom (Ordered Pairs) (a, b) = (c, d) ⇐⇒ a = c ∧ b = d Q : Are you satisfied with the definitions above? Hengfeng Wei (hfwei@nju.edu.cn) 1-9 Set Theory (II): Relations 2019 年 12 月 03 日 5 / 51