Skip to content

Commit

Permalink
Merge branch 'main' of https://github.com/ctrekker/Deductive.jl into …
Browse files Browse the repository at this point in the history
…main
  • Loading branch information
ctrekker committed Jan 7, 2022
2 parents 251b274 + cb45c4d commit b1227d9
Show file tree
Hide file tree
Showing 5 changed files with 273 additions and 36 deletions.
13 changes: 12 additions & 1 deletion src/atomic.jl
Original file line number Diff line number Diff line change
@@ -1,9 +1,19 @@
export , atomize

"""
a ⊼ b
Not AND operator (NAND for short). The NAND operator is a functionally complete boolean operator, meaning all other boolean
operations can be expressed with only NAND operations.
"""
= LogicalOperation((x, y) -> !(x && y), :, 2, true, true)

"""
atomize(expr::AbstractExpression)
Converts an expression into its directly converted NAND-only form.
"""
# Reduce an expression to its atomic form using the NAND operation
atomize(s::LogicalSymbol) = s
function atomize(expr::LogicalExpression)
parts = atomize.(arguments(expr))
expr_op = operation(expr)
Expand All @@ -24,3 +34,4 @@ function atomize(expr::LogicalExpression)

throw(ErrorException("Expression contains unsupported atomic operator $(expr_op)"))
end
atomize(s::LogicalSymbol) = s
257 changes: 222 additions & 35 deletions src/expression.jl
Original file line number Diff line number Diff line change
@@ -1,23 +1,34 @@
export ¬, , , ,
export LogicalSymbol, istree, isnode, metadata, variables, operation, operations, arguments, parents, left, right, isassociative, iscommutative
export isunary, isbinary
export LogicalSymbol, istree, isnode, name, metadata, variables, operation, operations, arguments, parents, left, right, isassociative, iscommutative
export isunary, isbinary, argument_count
export @symbols


abstract type AbstractExpression end

"""
LogicalSymbol(name::Symbol, metadata::Any=nothing)
Represent a logical symbolically with a provided name. By default the attached metadata is set to `nothing`.
"""
struct LogicalSymbol <: AbstractExpression
name::Symbol
metadata::Any
end
LogicalSymbol(name::Symbol) = LogicalSymbol(name, nothing)
istree(::LogicalSymbol) = false
isnode(::LogicalSymbol) = true
"""
name(sym::LogicalSymbol)
The name of the symbol provided at instantiation. Equivalent to `symbol(sym)`.
"""
name(sym::LogicalSymbol) = sym.name
"""
metadata(sym::LogicalSymbol)
The metadata of the symbol provided at instantiation, if any. Returns `nothing` if none was provided.
"""
metadata(sym::LogicalSymbol) = sym.metadata
variables(sym::LogicalSymbol) = Set{LogicalSymbol}(LogicalSymbol[sym])
operations(::LogicalSymbol) = Set{LogicalOperation}([])
arguments(::LogicalSymbol) = AbstractExpression[]

Base.show(io::IO, sym::LogicalSymbol) = print(io, string(sym.name))
Base.hash(sym::LogicalSymbol, h::UInt) = hash(sym.name, hash(sym.metadata, h))
Base.:(==)(sym1::LogicalSymbol, sym2::LogicalSymbol) = sym1.name == sym2.name && isequal(metadata(sym1), metadata(sym2))
Expand All @@ -28,6 +39,18 @@ Base.copy(sym::LogicalSymbol) = sym
Base.deepcopy(sym::LogicalSymbol) = LogicalSymbol(name(sym), deepcopy(metadata(sym)))

# convenience macros
"""
Define any number of `LogicalSymbols` with the names provided.
# Examples
```julia-repl
julia> @symbols a # defines symbol `a` in the current scope
julia> @symbols b c d # defines symbols `a`, `b`, and `c`
julia> @symbols α β γ # defines symbols `α`, `β`, and `γ`
```
"""
macro symbols(syms...)
definitions = [:(
$(esc(sym)) = LogicalSymbol($(esc(Symbol))($(string(sym))))
Expand All @@ -39,24 +62,62 @@ macro symbols(syms...)
end


"""
LogicalOperation(bool_fn::Function, name::Symbol, argument_count::Int, associative::Bool, commutative::Bool)
Defines a logical operator which can be used to form expressions with. Usually you don't need to define your own
operators, just use the ones built-in to the package if possible.
"""
struct LogicalOperation
bool_fn::Function
name::Symbol
argument_count::Int
associative::Bool
commutative::Bool
end
"""
argument_count(op::LogicalOperation)
The number of arguments which the given operation expects to receive.
"""
argument_count(op::LogicalOperation) = op.argument_count
"""
isunary(op::LogicalOperation)
True if the given operation only receives one argument, false otherwise.
"""
isunary(op::LogicalOperation) = argument_count(op) == 1
"""
isbinary(op::LogicalOperation)
True if the given operation receives two arguments, false otherwise.
"""
isbinary(op::LogicalOperation) = argument_count(op) == 2
"""
isassociative(op::LogicalOperation)
True if the given operation is associative, false otherwise.
"""
isassociative(op::LogicalOperation) = op.associative
"""
iscommutative(op::LogicalOperation)
True if the given operation is commutative, false otherwise.
"""
iscommutative(op::LogicalOperation) = op.commutative
Base.show(io::IO, op::LogicalOperation) = print(io, string(op.name))
Base.hash(op::LogicalOperation, h::UInt) = hash(op.name, hash(argument_count(op), hash(op.associative, hash(op.commutative, h))))
function Base.:(==)(op1::LogicalOperation, op2::LogicalOperation)
op1.name == op2.name && argument_count(op1) == argument_count(op2) && isassociative(op1) == isassociative(op2) && iscommutative(op1) == iscommutative(op2)
end

"""
(op::LogicalOperation)(args::AbstractExpression...)
This function is the foundation of expression building, as it allows instances of `LogicalOperations` to be treated as real
Julia functions. When called this function returns a `LogicalExpression` representing the application of the given operator
on the provided arguments.
"""
function (op::LogicalOperation)(args::AbstractExpression...)
if length(args) != argument_count(op)
throw(ErrorException("Invalid argument count $(length(args)). Expected $(argument_count(op)) arguments."))
Expand All @@ -69,6 +130,12 @@ end

recursivevariables(args::Vector{AbstractExpression}) = reduce(, variables.(args))
recursiveoperations(args::Vector{AbstractExpression}, rootop::LogicalOperation) = reduce(, operations.(args)) Set([rootop])
"""
LogicalExpression(arguments::Vector{AbstractExpression}, operation::LogicalOperation)
Constructs an expression with given arguments and logical operation. Please refrain from using this syntax, instead using
the "operators as functions" syntax, where a `LogicalOperation` instance can be called to produce a `LogicalExpression`.
"""
mutable struct LogicalExpression <: AbstractExpression
arguments::Vector{AbstractExpression}
operation::LogicalOperation
Expand All @@ -86,11 +153,26 @@ mutable struct LogicalExpression <: AbstractExpression
expr
end
end
istree(::LogicalExpression) = true
isnode(::LogicalExpression) = false
"""
operation(expr::LogicalExpression)
The operation which is performed on the arguments of the given `LogicalExpression`.
"""
operation(expr::LogicalExpression) = getfield(expr, :operation)
arguments(expr::LogicalExpression) = getfield(expr, :arguments)
"""
parents(expr::LogicalExpression)
The parent expressions of a given subexpression. If an expression is never used within another, it will have no parents.
In most expressions there will only be one parent, but it is possible for an expression assigned to a variable to have
multiple parents by using it as a "named subexpression".
"""
parents(expr::LogicalExpression) = getfield(expr, :parents)

"""
add_to_parents!(expr::LogicalExpression)
Adds an expression to the `parents` set of all its arguments. For internal use only.
"""
add_to_parents!(expr::LogicalExpression) = add_to_parents!(expr, arguments(expr))
function add_to_parents!(expr::LogicalExpression, relevant_args::Vector{AbstractExpression})
for arg relevant_args
Expand All @@ -99,6 +181,12 @@ function add_to_parents!(expr::LogicalExpression, relevant_args::Vector{Abstract
end
end
end

"""
remove_from_parents!(expr::LogicalExpression)
Removes an expression from the `parents` set of all its arguments. For internal use only.
"""
remove_from_parents!(expr::LogicalExpression) = remove_from_parents!(expr, arguments(expr))
function remove_from_parents!(expr::LogicalExpression, relevant_args::Vector{AbstractExpression})
for arg relevant_args
Expand All @@ -108,23 +196,29 @@ function remove_from_parents!(expr::LogicalExpression, relevant_args::Vector{Abs
end
end
metadata(::LogicalExpression) = nothing
function variables(expr::LogicalExpression)
if !getfield(expr, :cached_variables_valid)
setfield!(expr, :cached_variables, recursivevariables(arguments(expr)))
expr.cached_variables_valid = true
end
getfield(expr, :cached_variables)
end
function operations(expr::LogicalExpression)
if !getfield(expr, :cached_operations_valid)
setfield!(expr, :cached_operations, recursiveoperations(arguments(expr), operation(expr)))
expr.cached_operations_valid = true
end
getfield(expr, :cached_operations)
end
"""
left(expr::LogicalExpression)
If the expression is binary, this method returns the left-hand operand.
"""
left(expr::LogicalExpression) = isbinary(operation(expr)) ? arguments(expr)[1] : throw(ErrorException("Operation $(operation(expr)) is not binary"))
"""
right(expr::LogicalExpression)
If the expression is binary, this method returns the right-hand operand.
"""
right(expr::LogicalExpression) = isbinary(operation(expr)) ? arguments(expr)[2] : throw(ErrorException("Operation $(operation(expr)) is not binary"))
"""
isassociative(expr::LogicalExpression)
Checks if the entire expression is associative based on the associative property of its constituent operations.
"""
isassociative(expr::LogicalExpression) = length(operations(expr)) == 1 && isassociative(operation(expr))
"""
iscommutative(expr::LogicalExpression)
Checks if the entire expression is commutative based on the commutative property of its constituent operations.
"""
iscommutative(expr::LogicalExpression) = length(operations(expr)) == 1 && iscommutative(operation(expr))
Base.hash(expr::LogicalExpression, h::UInt) = hash(arguments(expr), hash(operation(expr), h))
Base.:(==)(expr1::LogicalExpression, expr2::LogicalExpression) = operation(expr1) == operation(expr2) && all(arguments(expr1) .== arguments(expr2))
Expand Down Expand Up @@ -185,12 +279,6 @@ function setvectorindex!(expr::LogicalExpression, name::Symbol, x, index::Union{
end
end

function set_argument(expr::LogicalExpression, index::Int, new_argument::AbstractExpression)
expr.arguments[index] = new_argument
expr.variables = reduce(, variables.(arguments(expr)))
expr
end


function Base.show(io::IO, expr::LogicalExpression)
showparens(expr) = (expr isa LogicalExpression) && !isunary(operation(expr))
Expand Down Expand Up @@ -231,17 +319,92 @@ function Base.show(io::IO, expr::LogicalExpression)
end


# ASSOCIATION
associative_ordering(sym::LogicalSymbol) = [sym]
# Standard AbstractExpression interface methods
"""
istree(expr::T) where {T <: AbstractExpression}
Returns true when `expr` is a `LogicalExpression` and false otherwise.
"""
istree(::LogicalSymbol) = false
istree(::LogicalExpression) = true

"""
isnode(expr::T) where {T <: AbstractExpression}
Returns true when `expr` is a `LogicalSymbol` and false otherwise.
"""
isnode(::LogicalSymbol) = true
isnode(::LogicalExpression) = false

"""
variables(expr::T) where {T <: AbstractExpression}
Returns variables present in an entire expression tree. When the first argument is a `LogicalSymbol`, this is singleton
set containing only the provided `LogicalSymbol`. When the argument is a `LogicalExpression`, this is a set containing the union
of all the variables present in each argument.
"""
variables(sym::LogicalSymbol) = Set{LogicalSymbol}(LogicalSymbol[sym])
function variables(expr::LogicalExpression)
if !getfield(expr, :cached_variables_valid)
setfield!(expr, :cached_variables, recursivevariables(arguments(expr)))
expr.cached_variables_valid = true
end
getfield(expr, :cached_variables)
end

"""
operations(expr::T) where {T <: AbstractExpression}
Returns the operations present in an entire expression tree. When given a `LogicalSymbol`, this is an empty set, whereas
when given a `LogicalExpression`, this is a set containing the expression's own `LogicalOperation` and the operations set
of each of its arguments.
"""
operations(::LogicalSymbol) = Set{LogicalOperation}([])
function operations(expr::LogicalExpression)
if !getfield(expr, :cached_operations_valid)
setfield!(expr, :cached_operations, recursiveoperations(arguments(expr), operation(expr)))
expr.cached_operations_valid = true
end
getfield(expr, :cached_operations)
end

"""
arguments(expr::T) where {T <: AbstractExpression}
Returns the arguments which an `AbstractExpression` contains. `LogicalSymbols` contain no arguments and `LogicalExpressions`
can contain any number of arguments.
"""
arguments(::LogicalSymbol) = AbstractExpression[]
arguments(expr::LogicalExpression) = getfield(expr, :arguments)


# ASSOCIATION (perhaps move this elsewhere eventually?)
"""
associative_ordering(expr::LogicalExpression)
Descends the expression tree with a left-side-first depth first search. Each symbol encountered is added to a list in
the order it appears in this search and is returned by this function.
"""
associative_ordering(expr::LogicalExpression) = reduce(vcat, associative_ordering.(arguments(expr)))
associative_ordering(sym::LogicalSymbol) = [sym]

isequal_associative(sym1::LogicalSymbol, sym2::LogicalSymbol) = isequal(sym1, sym2)
"""
isequal_associative(expr1::LogicalExpression, expr2::LogicalExpression)
Checks whether an expression is equal with another ignoring the associative ordering of each expression.
"""
function isequal_associative(expr1::LogicalExpression, expr2::LogicalExpression)
length(operations(expr1)) == 1 && operations(expr1) == operations(expr2) && associative_ordering(expr1) == associative_ordering(expr2)
length(operations(expr1)) == 1 && isassociative(first(operations(expr1))) && operations(expr1) == operations(expr2) && associative_ordering(expr1) == associative_ordering(expr2)
end
isequal_associative(sym1::LogicalSymbol, sym2::LogicalSymbol) = isequal(sym1, sym2)
isequal_associative(::AbstractExpression, ::AbstractExpression) = false

_associative_tree_count_cache = Dict()
"""
associative_tree_count(nodes::Int)
Function which calculates how many ways to arrange parenthesis in an expression there are with a given node count.
"""
function associative_tree_count(nodes::Int)
if nodes == 0
return 1
Expand All @@ -266,11 +429,35 @@ end


# OPERATORS
# unary operator
"""
¬(x)
Logical negation operator, typed with `\\neg`. Boolean equivalent is the `!` operator.
"""
const ¬ = LogicalOperation(x -> !x, :¬, 1, false, false)

# binary operators
"""
x ∧ y
Logical conjunction operator, typed with `\\wedge`. Boolean equivalent is the `&&` operator.
"""
const = LogicalOperation((x, y) -> x && y, :, 2, true, true)
"""
x ∨ y
Logical disjunction operator, typed with `\\vee`. Boolean equivalent is the `||` operator.
"""
const = LogicalOperation((x, y) -> x || y, :, 2, true, true)
"""
x → y
Logical implication operator, typed with `\\rightarrow`.
"""
const = LogicalOperation((x, y) -> (¬x y), :, 2, false, false)
"""
x ⟷ y
Logical equivalence operator, typed with `\\longleftrightarrow`.
"""
const = LogicalOperation((x, y) -> (x y) (¬x ¬y), :, 2, true, true)
Loading

2 comments on commit b1227d9

@ctrekker
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@JuliaRegistrator
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Registration pull request created: JuliaRegistries/General/51860

After the above pull request is merged, it is recommended that a tag is created on this repository for the registered package version.

This will be done automatically if the Julia TagBot GitHub Action is installed, or can be done manually through the github interface, or via:

git tag -a v0.0.5 -m "<description of version>" b1227d9cb5e9be3aeb3f769f1041d1ac6a9a6f4d
git push origin v0.0.5

Please sign in to comment.