diff --git a/src/atomic.jl b/src/atomic.jl index 264fde0..06eab5f 100644 --- a/src/atomic.jl +++ b/src/atomic.jl @@ -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) @@ -24,3 +34,4 @@ function atomize(expr::LogicalExpression) throw(ErrorException("Expression contains unsupported atomic operator $(expr_op)")) end +atomize(s::LogicalSymbol) = s diff --git a/src/expression.jl b/src/expression.jl index 92639bd..9d8de37 100644 --- a/src/expression.jl +++ b/src/expression.jl @@ -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)) @@ -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)))) @@ -39,6 +62,12 @@ 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 @@ -46,10 +75,35 @@ struct LogicalOperation 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)))) @@ -57,6 +111,13 @@ 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.")) @@ -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 @@ -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 @@ -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 @@ -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)) @@ -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)) @@ -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 @@ -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) diff --git a/src/inference.jl b/src/inference.jl index 8fc55f9..9562474 100644 --- a/src/inference.jl +++ b/src/inference.jl @@ -8,6 +8,12 @@ export @logical_calculus, InferenceRule, PropositionalCalculus, ⊢ Statement = AbstractExpression StatementSet = Set{Statement} +""" + InferenceRule(name::String, premise::StatementSet, conclusion::Statement) + +Define a rule which maps a set of statements to a logical conclusion. The name is cited each time +a rule is applied in a proof step. +""" struct InferenceRule name::String premise::StatementSet @@ -28,6 +34,11 @@ function _leaf_symbols(expr::Expr) Set(Iterators.flatten(_leaf_symbols.(args))) end +""" +Defines a logical calculus based on a set of inference rules which can be applied repeatedly to +a given set of statements (premises). See `PropositionalCalculus` for an example definition using +this macro. +""" macro logical_calculus(var, defs) rules_list = defs.args[2].args @@ -59,6 +70,11 @@ macro logical_calculus(var, defs) end +""" + A ⊢ B + +Provability operator used exclusively in calculus definitions. A ⊢ B means that B can be proven using A as the premise. +""" ⊢ = LogicalOperation((a, b) -> true, :⊢, 2, false, false) @logical_calculus PropositionalCalculus begin @@ -141,6 +157,12 @@ end p ∨ r ), q end +""" + PropositionalCalculus + +Default calculus definition for zeroth-order (propositional) logic. +""" +PropositionalCalculus @logical_calculus ExtendedPropositionalCalculus begin # Rules for negations diff --git a/src/search.jl b/src/search.jl index 8dff62e..ea9627c 100644 --- a/src/search.jl +++ b/src/search.jl @@ -3,6 +3,12 @@ export contains_expression # SUBEXPRESSION SEARCH # if haystack is a logical symbol, the kneedle must be equal to be a subexpression +""" + contains_expression(haystack::AbstractExpression, kneedle::AbstractExpression) + +Searches for a subexpression `kneedle` recursively within the `haystack` expression. Returns true if a match can be found +and false otherwise. +""" contains_expression(haystack::LogicalSymbol, kneedle::AbstractExpression) = isequal(haystack, kneedle) # TODO: come up with quicker subexpression algorithm for LogicalExpressions diff --git a/src/utils.jl b/src/utils.jl index 5bbf245..1010789 100644 --- a/src/utils.jl +++ b/src/utils.jl @@ -1,5 +1,16 @@ +""" + flat_repeat(x, n) + +Shortcut for `Iterators.repeat([x], n)` +""" flat_repeat(x, n) = Iterators.repeat([x], n) +""" + FakeVector{X, T}(creator::X, fieldname::Symbol, vec::Vector{T}) + +A utility structure which calls a function `setvectorindex!` when the `Base.setindex!` function is called on it. This +allows for some smart updating of expression trees when mutated. +""" struct FakeVector{X, T} creator::X fieldname::Symbol