Operators
Operators accept Bools, truth values, and propositions. However, boolean values cannot interoperate with truth values and propositions. Operations on boolean values is always eagerly evaluated, whereas operations on truth values and propositions is evaluated according to the operator's Evaluation trait.
Operations on propositions that have each been normalized eagerly evaluate to another normalized proposition. This behavior is likely to be removed in v0.4.
Typing symbols with tab completion is performed by typing \, followed by the given characters, and then the [TAB] key. For example, ⊤ is typed with \top[TAB]. See also Tab Completion and Unicode Input.
Operator associativity determines how operators with the same precedence group their operands. For example, ∧ is left associative. Therefore, p ∧ q ∧ r is equivalent to (p ∧ q) ∧ r. Operator precedence determines how expressions with distinct operators are grouped together. Higher precedence operators will group their operands before lower precedence operators. For example, ∧ has a higher precedence than ∨. Therefore, p ∨ q ∧ r is equivalent to p ∨ (q ∧ r), even though both operators are left associative. See also Julia's documentation on Operator Precedence and Associativity.
This associativity is determined by Julia's parser and is distinct from the Associativity trait used to specify the direction an operator folds.
== has a precedence of 7, which is higher than that of several binary operators. For those cases, you may need to use parentheses. For example, p → q == r parses as p → (q == r) rather than (p → q) == r.
| Name | Symbol | Tab Completion | Associativity | Precedence |
|---|---|---|---|---|
tautology | ⊤ | \top | none | 0 |
contradiction | ⊥ | \bot | none | 0 |
identical | 𝒾 | \scri | none | 0 |
not | ¬ | \neg | right | 0 |
and | ∧ | \wedge | left | 12 |
or | ∨ | \vee | left | 11 |
imply | → | \rightarrow | right | 4 |
exclusive_or | ↮ | \nleftrightarrow | right | 4 |
converse_imply | ← | \leftarrow | right | 4 |
not_and | ↑ | \uparrow | right | 15 |
not_or | ↓ | \downarrow | right | 15 |
not_imply | ↛ | \nrightarrow | right | 4 |
not_exclusive_or | ↔ | \leftrightarrow | right | 4 |
not_converse_imply | ↚ | \nleftarrow | right | 4 |
conjunction | ⋀ | \bigwedge | none | 0 |
disjunction | ⋁ | \bigvee | none | 0 |
Nullary Operators
PAndQ.tautology — Constanttautology()
⊤()Logical true operator.
⊤ can be typed by \top[TAB].
Examples
julia> print_table(⊤)
┌───┐
│ ⊤ │
├───┤
│ ⊤ │
└───┘PAndQ.contradiction — Constantcontradiction()
⊥()Logical false operator.
⊥ can be typed by \bot[TAB].
Examples
julia> print_table(⊥)
┌───┐
│ ⊥ │
├───┤
│ ⊥ │
└───┘Unary Operators
PAndQ.identical — Constantidentical(p)
𝒾(p)Logical identity operator.
Examples
julia> @atomize print_table(𝒾(p))
┌───┐
│ p │
├───┤
│ ⊤ │
│ ⊥ │
└───┘PAndQ.not — Constantnot(p)
¬pLogical negation operator.
¬ can be typed by \neg[TAB].
Examples
julia> @atomize print_table(¬p)
┌───┬────┐
│ p │ ¬p │
├───┼────┤
│ ⊤ │ ⊥ │
│ ⊥ │ ⊤ │
└───┴────┘Binary Operators
PAndQ.and — Constantand(p, q)
p ∧ qLogical conjunction operator.
∧ can be typed by \wedge[TAB].
Examples
julia> @atomize print_table(p ∧ q)
┌───┬───┬───────┐
│ p │ q │ p ∧ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊤ │
│ ⊥ │ ⊤ │ ⊥ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊥ │
│ ⊥ │ ⊥ │ ⊥ │
└───┴───┴───────┘PAndQ.or — Constantor(p, q)
p ∨ qLogical disjunction operator.
∨ can be typed by \vee[TAB].
Examples
julia> @atomize print_table(p ∨ q)
┌───┬───┬───────┐
│ p │ q │ p ∨ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊤ │
│ ⊥ │ ⊤ │ ⊤ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊤ │
│ ⊥ │ ⊥ │ ⊥ │
└───┴───┴───────┘PAndQ.imply — Constantimply(p, q)
p → qLogical implication operator.
→ can be typed by \rightarrow[TAB].
Examples
julia> @atomize print_table(p → q)
┌───┬───┬───────┐
│ p │ q │ p → q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊤ │
│ ⊥ │ ⊤ │ ⊤ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊥ │
│ ⊥ │ ⊥ │ ⊤ │
└───┴───┴───────┘PAndQ.exclusive_or — Constantexclusive_or(p, q)
p ↮ qLogical exclusive disjunction operator.
↮ can be typed by \nleftrightarrow[TAB].
Examples
julia> @atomize print_table(p ↮ q)
┌───┬───┬───────┐
│ p │ q │ p ↮ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊥ │
│ ⊥ │ ⊤ │ ⊤ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊤ │
│ ⊥ │ ⊥ │ ⊥ │
└───┴───┴───────┘PAndQ.converse_imply — Constantconverse_imply(p, q)
p ← qLogical converse implication operator.
← can be typed by \leftarrow[TAB].
Examples
julia> @atomize print_table(p ← q)
┌───┬───┬───────┐
│ p │ q │ p ← q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊤ │
│ ⊥ │ ⊤ │ ⊥ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊤ │
│ ⊥ │ ⊥ │ ⊤ │
└───┴───┴───────┘PAndQ.not_and — Constantnot_and(p, q)
p ↑ qLogical non-conjunction operator.
↑ can be typed by \uparrow[TAB].
Examples
julia> @atomize print_table(p ↑ q)
┌───┬───┬───────┐
│ p │ q │ p ↑ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊥ │
│ ⊥ │ ⊤ │ ⊤ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊤ │
│ ⊥ │ ⊥ │ ⊤ │
└───┴───┴───────┘PAndQ.not_or — Constantnot_or(p, q)
p ↓ qLogical non-disjunction operator.
↓ can be typed by \downarrow[TAB].
Examples
julia> @atomize print_table(p ↓ q)
┌───┬───┬───────┐
│ p │ q │ p ↓ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊥ │
│ ⊥ │ ⊤ │ ⊥ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊥ │
│ ⊥ │ ⊥ │ ⊤ │
└───┴───┴───────┘PAndQ.not_imply — Constantnot_imply(p, q)
p ↛ qLogical non-implication operator.
↛ can be typed by \nrightarrow[TAB].
Examples
julia> @atomize print_table(p ↛ q)
┌───┬───┬───────┐
│ p │ q │ p ↛ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊥ │
│ ⊥ │ ⊤ │ ⊥ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊤ │
│ ⊥ │ ⊥ │ ⊥ │
└───┴───┴───────┘PAndQ.not_exclusive_or — Constantnot_exclusive_or(p, q)
p ↔ qLogical exclusive non-disjunction operator.
↔ can be typed by \leftrightarrow[TAB].
Examples
julia> @atomize print_table(p ↔ q)
┌───┬───┬───────┐
│ p │ q │ p ↔ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊤ │
│ ⊥ │ ⊤ │ ⊥ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊥ │
│ ⊥ │ ⊥ │ ⊤ │
└───┴───┴───────┘PAndQ.not_converse_imply — Constantnot_converse_imply(p, q)
p ↚ qLogical converse non-implication operator.
↚ can be typed by \nleftarrow[TAB].
Examples
julia> @atomize print_table(p ↚ q)
┌───┬───┬───────┐
│ p │ q │ p ↚ q │
├───┼───┼───────┤
│ ⊤ │ ⊤ │ ⊥ │
│ ⊥ │ ⊤ │ ⊤ │
├───┼───┼───────┤
│ ⊤ │ ⊥ │ ⊥ │
│ ⊥ │ ⊥ │ ⊥ │
└───┴───┴───────┘Nary Operators
PAndQ.conjunction — Constantconjunction(ps)
⋀(ps)Equivalent to fold(𝒾, (∧) => ps).
⋀ can be typed by \bigwedge[TAB].
See also identical, and, and fold.
Examples
julia> ⋀(())
⊤
julia> @atomize ⋀((p, q, r, s))
((p ∧ q) ∧ r) ∧ sPAndQ.disjunction — Constantdisjunction(ps)
⋁(ps)Equivalent to fold(𝒾, (∨) => ps).
⋁ can be typed by \bigvee[TAB].
See also identical, or, and fold.
Examples
julia> ⋁(())
⊥
julia> @atomize ⋁((p, q, r, s))
((p ∨ q) ∨ r) ∨ sUtilities
PAndQ.fold — Functionfold(f, pairs...)A generalization of mapreduce with an arbitrary number of nested folds and traits to determine each operator's Associativity and initial_value.
The function f must accept as many parameters as there are pairs. Each pair must be a two element iterable where the first element is a binary operator and the second element is an iterable to be folded over.
Given a single pair, this function is similar to mapreduce and other similar functions. Giving additional pairs will generalize the following pattern:
mapreduce(a, xs) do x
mapreduce(b, ys) do y
...
end
endThis can be rewritten as:
fold(a => xs, b => ys, ...) do x, y, ...
...
endExamples
julia> fold(⊤)
⊤
julia> @atomize fold(¬, (∧) => (p, q))
¬p ∧ ¬q
julia> @atomize fold(↔, (∧) => (p, q), (∨) => (r, s))
((p ↔ r) ∨ (p ↔ s)) ∧ ((q ↔ r) ∨ (q ↔ s))