Propositions
Instantiation
PAndQ.@atomize
— Macro@atomize(x)
Instantiate constants and variables inline.
Constants are instantiated with the $
interpolation syntax. Variables are instantiated with previously undefined symbols.
This macro attempts to ignore symbols that are being assigned a value. For example, @atomize f(; x = p) = x ∧ q
should be equivalent to f(; x = @atomize p) = x ∧ @atomize q
. However, this feature is in-progress and only works in some cases. The implementation is cautious to skip the parts of the expression that it cannot yet handle.
Examples
julia> @atomize x = p ∧ q
p ∧ q
julia> @atomize x → r
(p ∧ q) → r
julia> @atomize $1 ∧ $(1 + 1)
$(1) ∧ $(2)
PAndQ.@variables
— Macro@variables(ps...)
Define variables and return a Vector
containing them.
Examples
julia> @variables p q
2-element Vector{PAndQ.AbstractSyntaxTree}:
p
q
julia> p
p
julia> q
q
PAndQ.constants
— Functionconstants(f = identity, xs)
Equivalent to map(x -> @atomize $(f(x)), xs)
.
See also identical
.
Examples
julia> constants(1:2)
2-element Vector{PAndQ.AbstractSyntaxTree}:
$(1)
$(2)
julia> constants(string, 1:2)
2-element Vector{PAndQ.AbstractSyntaxTree}:
$("1")
$("2")
Utilities
PAndQ.value
— Functionvalue(T = Any, p)
If p
is logically equivalent to a constant, return that constant's value wrapped in Some
. Otherwise, return nothing
.
Values wrapped in Some
can be unwrapped using the something
function.
To reduce compilation latency, constants do not store the type of the wrapped value. Therefore, the type of this value cannot be inferred and can result in run-time dispatch. If this type is known at compile-time, pass it as the first parameter. See also the performance tip to Annotate values taken from untyped locations.
Examples
julia> @atomize value(p)
julia> @atomize value($1)
Some(1)
julia> @atomize something(value(Int, $2))
2
Base.map
— Functionmap(f, p)
Apply the function f
to each atom in p
.
Examples
julia> @atomize map(¬, p ∧ q)
¬p ∧ ¬q
julia> @atomize map(atom -> $(something(value(atom)) + 1), $1 ∧ $2)
$(2) ∧ $(3)
PAndQ.atoms
— Functionatoms(p)
Return an iterator of each atomic proposition contained in p
.
Examples
julia> @atomize collect(atoms(p ∧ q))
2-element Vector{PAndQ.AbstractSyntaxTree}:
p
q
PAndQ.install_atomize_mode
— Functioninstall_atomize_mode(;
start_key = "\M-a", prompt_text = "atomize> ", prompt_color = :cyan,
kwargs...)
Install the atomize
REPL mode, where input implicitly begins with @atomize
.
Keyword arguments are passed to ReplMaker.initrepl
. The default start keys are pressing both the [Meta] (also known as [Alt]) and [a] keys at the same time. The available prompt_color
s are in Base.text_colors
.
Normalization
PAndQ.normalize
— Functionnormalize(::typeof(¬), p)
normalize(::Union{typeof(∧), typeof(∨)}, p; canonical = false)
Convert the given proposition to negation, conjunction, or disjunction normal form depending on whether the first argument is not
, and
, or or
, respectively.
Considering the syntax tree of a normalized proposition, each leaf node is a literal; either an atom or it's negation. Propositions in negation normal form are expanded such that the syntax tree branches only contain the operators and
and or
. Conjunction and disjunction normal forms are negated normal forms that have been flattened by recursively distributing either the and
or or
operator over the other. In other words, a collection of literals is a clause and a proposition in conjunctive or disjunctive normal form is a conjunction of disjunctive clauses or a disjunction of conjunctive clauses, respectively.
Conjunction and disjunction, but not negation, normal forms are called canonical. Distributing an operator during conversion may increase the size of the syntax tree exponentially. Therefore, it may be intractable to compute a canonical form for sufficiently large propositions. Instead, use the tseytin
transformation to find a proposition in conjunctive normal form which is_equisatisfiable
to the given proposition.
Converting a proposition between conjunction and disjunction normal form is not performant due to the exponential increase in the size of the proposition. It is most performant to apply all operations to propositions and normalizing the resulting proposition once.
Examples
julia> @atomize normalize(∧, ¬(p ∨ q))
¬q ∧ ¬p
julia> @atomize normalize(∨, p ↔ q)
(¬q ∧ ¬p) ∨ (p ∧ q)
PAndQ.tseytin
— Functiontseytin(p)
Apply the Tseytin transformation to the given proposition.
Using the normalize
function to convert a proposition to conjunction normal form may result in an exponentially larger proposition, which can be intractable for sufficiently large propositions. The Tseytin transformation results in a linearly larger proposition that is in conjunction normal form and is_equisatisfiable
to the original. However, it contains introduced variables and yields a subset of the solutions
to the original proposition.
Examples
julia> is_equisatisfiable(⊤, tseytin(⊤))
true
julia> @atomize is_equisatisfiable(p, tseytin(p))
true
julia> is_equisatisfiable(⊥, tseytin(⊥))
true