Operators
Operators accept Bool
s, 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 normalize
d 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 fold
s.
==
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)
¬p
Logical negation operator.
¬
can be typed by \neg[TAB]
.
Examples
julia> @atomize print_table(¬p)
┌───┬────┐
│ p │ ¬p │
├───┼────┤
│ ⊤ │ ⊥ │
│ ⊥ │ ⊤ │
└───┴────┘
Binary Operators
PAndQ.and
— Constantand(p, q)
p ∧ q
Logical 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 ∨ q
Logical 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 → q
Logical 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 ↮ q
Logical 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 ← q
Logical 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 ↑ q
Logical 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 ↓ q
Logical 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 ↛ q
Logical 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 ↔ q
Logical 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 ↚ q
Logical 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 ∧ s
PAndQ.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 ∨ s
Utilities
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
end
This can be rewritten as:
fold(a => xs, b => ys, ...) do x, y, ...
...
end
Examples
julia> fold(⊤)
⊤
julia> @atomize fold(¬, (∧) => (p, q))
¬p ∧ ¬q
julia> @atomize fold(↔, (∧) => (p, q), (∨) => (r, s))
((p ↔ r) ∨ (p ↔ s)) ∧ ((q ↔ r) ∨ (q ↔ s))