Skip to content

Instantly share code, notes, and snippets.

@yohhoy

yohhoy/subsume-P0717R1.txt

Last active Sep 11, 2019
Embed
What would you like to do?
C++20 Concepts constraints subsumption analysis
constraint-expressions:
- C1<T>^c && C2<T>^c
- C1<T>^d
# concept version
template <class T> concept C1<T> = true^a;
template <class T> concept C2<T> = true^b;
normal form of P = true^a ∧ true^b
normal form of Q = true^a
P_1 = (true^a ∧ true^b)
Q_1 = (true^a)
⇒ P_11=(true^a) identical Q_11=(true^a) ⇒ P_11 subsume Q_11
⇒ (true^a && true^b) subsume (true^a)
normal form of P = true^a
normal form of Q = true^a ∧ true^b
P_1 = (true^a)
Q_1 = (true^a), Q_2=(true^b)
{ P_11=(true^a) identical Q_11=(true^a) ⇒ P_11 subsume Q_11,
P_11=(true^a) NOT identical Q_21=(true^b) ⇒ P_11 NOT subsume Q_21 }
⇒ (true^a) NOT subsume (true^a && true^b)
# non-concept version
template <class T> inline constexpr bool C1<T> = true^a;
template <class T> inline constexpr bool C2<T> = true^b;
normal form of P = C1<T>^c ∧ C2<T>^c
normal form of Q = C1<T>^d
P_1 = (C1<T>^c ∧ C2<T>^c)
Q_1 = (C1<T>^d)
{ P_11=(C1<T>^c) NOT identical Q_11=(C1<T>^c) ⇒ P_11 NOT subsume Q_11,
{ P_12=(C2<T>^c) NOT identical Q_11=(C1<T>^c) ⇒ P_12 NOT subsume Q_11 }
⇒ (C1<T>^c && C2<T>^c) NOT subsume (C1<T>^d)
normal form of P = C1<T>^d
normal form of Q = C1<T>^c ∧ C2<T>^c
P_1 = (C1<T>^d)
Q_1 = (C1<T>^c), Q_2 = (C2<T>^c)
{ P_11=(C1<T>^d) NOT identical Q_11=(C1<T>^c) ⇒ P_11 NOT subsume Q_11,
P_11=(C1<T>^d) NOT identical Q_21=(C2<T>^c) ⇒ P_11 NOT subsume Q_21 }
⇒ (C1<T>^d) NOT subsume (C1<T>^c && C2<T>^c)
constraint-expressions:
- C1<T> && C2<T>
- C1<T>
# concept version
template <class T> concept C1<T> = true;
template <class T> concept C2<T> = true;
normal form of P = true ∧ true
normal form of Q = true
P_1 = (true ∧ true)
Q_1 = (true)
⇒ P_11=(true) identical Q_11=(true) ⇒ P_11 subsume Q_11
⇒ (true && true) subsume (true)
normal form of P = true
normal form of Q = true ∧ true
P_1 = (true)
Q_1 = (true), Q_2=(true)
{ P_11=(true) identical Q_11=(true) ⇒ P_11 subsume Q_11,
P_11=(true) identical Q_21=(true) ⇒ P_11 subsume Q_21 }
⇒ true subsume (true && true)
# non-concept version
template <class T> inline constexpr bool C1<T> = true;
template <class T> inline constexpr bool C2<T> = true;
normal form of P = C1<T> ∧ C2<T>
normal form of Q = C1<T>
P_1 = (C1<T> ∧ C2<T>)
Q_1 = (C1<T>)
⇒ P_11=(C1<T>) identical Q_11=(C1<T>) ⇒ P_11 subsume Q_11
⇒ (C1<T> && C2<T>) subsume (C1<T>)
normal form of P = C1<T>
normal form of Q = C1<T> ∧ C2<T>
P_1 = (C1<T>)
Q_1 = (C1<T>), Q_2 = (C2<T>)
{ P_11=(C1<T>) identical Q_11=(C1<T>) ⇒ P_11 subsume Q_11,
P_11=(C1<T>) NOT identical Q_21=(C2<T>) ⇒ P_11 NOT subsume Q_21 }
⇒ C1<T> NOT subsume (C1<T> && C2<T>)
@yohhoy

This comment has been minimized.

Copy link
Owner Author

@yohhoy yohhoy commented Sep 11, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.