Association rule mining with modal logic

Symbolic modal learning is a branch of machine learning which deals with training classical symbolic machine learning models (e.g., list and set of rules, decision trees, random forests, association rules, etc.) but substituting propositional logic with a more expressive logical formalism (yet, computationally more affordable than first order logic), that is, a specific kind of modal logic.

In the context of this package, modal logic helps us highlight complex relations hidden in data, especially in unstructured data, consisting of graph-like relational data, time series, spatial databases, text, etc. For more information about the modal symbolic learning, we suggest reading the main page of Sole.jl framework and SoleLogics.jl.

The idea is to discretize complex data into relational objects called Kripke models, each of which consists of many propositional models called worlds, and expliciting the relations between worlds. In this way, it is possible to mine complex Itemset, including a certain subset of Item that are true on a target world, but also modally enhanced items that are true on related worlds.

A picture is worth a thousand words. Here you are a slightly more complex example, with respect to the one at the top of Getting started section. We consider this monovariate time series:

We want to encode a graph-like structure from the data above. We could think of various strategies, one of which is to consider every contiguous subsequence in the time series and model it as a set of intervals.

At this point, we can see every resulting blue signal as a propositional model, on which items may be evaluated as true or false. In the modal logic jargon, this is exactly a Kripke model.

After fixing a set of suitable relations, we express them with arcs in the structure. Without defining them, we graphically present some possible relations between intervals. The one below is the begins relation.

Conversely, this one is the ends relation.

When an interval is completely included in another one, then we say that it happens during the other one.

Finally, we say that an interval comes just after another one if its end coincides with the beginning of the other one.

Every relation $R$ can be declined in an existential or a universal way. In the former (latter) case, given an item $p$, we say that $<R>p$ is true on $w$ if at least one world (all worlds) $w'$ is such that $wRw'$ and $p$ is true on $w'$. Such relations can be encoded thanks to SoleLogics.jl; in particular, we use diamond(relation_name) to indicate an existential modality while box(relation_name) to indicate universal ones:

myitem = ScalarCondition(VariableDistance(1, [1,2,3]), <=, 1.0) |> diamond(IA_L)

Meaningfulness measures

We already introduced lsupport, gsupport, lconfidence and gconfidence in the Getting started section. Other measures that are already built into the package, are the following; note how their definition always depends on the notion of lsupport, and they are always organized in both local and global versions.

Local means that a measure is designed to be applied within a modal instance (a Kripke model), while global keywords denotes the fact that the computation is performed across instances.

function llift(
    rule::ARule,
    ith_instance::LogicalInstance;
    miner::Union{Nothing,AbstractMiner}=nothing
)::Float64

function glift(
    rule::ARule,
    X::SupportedLogiset,
    threshold::Threshold;
    miner::Union{Nothing,AbstractMiner}=nothing
)::Float64

function lconviction(
    rule::ARule,
    ith_instance::LogicalInstance;
    miner::Union{Nothing,AbstractMiner}=nothing
)::Float64

function gconviction(
    rule::ARule,
    X::SupportedLogiset,
    threshold::Threshold;
    miner::Union{Nothing,AbstractMiner}=nothing
)::Float64

function lleverage(
    rule::ARule,
    X::SupportedLogiset,
    threshold::Threshold;
    miner::Union{Nothing,AbstractMiner}=nothing
)::Float64

function gleverage(
    rule::ARule,
    X::SupportedLogiset,
    threshold::Threshold;
    miner::Union{Nothing,AbstractMiner}=nothing
)::Float64

In general, we can define new meaningfulness measures by leveraging the following macros, ensuring to avoid solving repeated subproblems when computing the measure.

macro localmeasure(measname, measlogic)

_lsupport_logic = (itemset, X, ith_instance, miner) -> begin
    # vector representing on which world an Itemset holds
    wmask = [
        check(formula(itemset), X, ith_instance, w) for w in allworlds(X, ith_instance)]

    # return the result enriched with more informations, that will eventually will be
    # used if miner's miningstate has specific fields (e.g., :worldmask).
    return Dict(
        :measure => count(wmask) / length(wmask),
        :worldmask => wmask,
    )
end

macro globalmeasure(measname, measlogic)

_gsupport_logic = (itemset, X, threshold, miner) -> begin
    _measure = sum([
        lsupport(itemset, getinstance(X, ith_instance), miner) >= threshold
        for ith_instance in 1:ninstances(X)
    ]) / ninstances(X)

    # at the moment, no `miningstate` fields in miner are leveraged
    return Dict(:measure => _measure)
end

You can identify which is the local (global) counterpart of a global (local) meaningfulness measure with the following utility dispatches.

islocalof(::Function, ::Function)::Bool

localof(::Function)::Union{Nothing,MeaningfulnessMeasure}

isglobalof(::Function, ::Function)::Bool

globalof(::Function)::Union{Nothing,MeaningfulnessMeasure} = nothing

Of course, you can even link your measures local-to-global and viceversa. See also findmeasure.

macro linkmeas(gmeasname, lmeasname)

Mining Algorithms

The core of every association rule mining workflow consists of extracting the frequent patterns from data. To explore the search space of all such patterns, we can use a "level-wise" approach, based on breadth-first search algorithm, called apriori, or a "vertical data format" approach, based on a depth-first search, called eclat.

eclat(miner::Miner, X::MineableData; verbose::Bool=true)::Nothing

We suggest to run fpgrowth, as it is the most performant algorithm among those implemented at the moment of writing. It is based on a compression strategy, based on iteratively "projecting" the initial dataset; projections are particular slicings of the initial dataset, keeping only the information needed for continuining the mining process.

Mining Policies

It is possible to limit the action of the mining, to force an AbstractMiner to only consider a subset of the available data.

We can also constrain the generation of new itemsets and rules by defining a vector of policies. Every policy is a closure returning a custom parameterized checker for a certain constraint.

For what regards itemsets, the following dispatches are available:

The following are referred to association rules:

To apply the policies, call the following.

Anchored semantics

To ensure the mining process is fair when dealing with modal operators, we must ensure that the miner is compliant with anchored semantics constraints.

To understand why the fairness of the frequent pattern extraction process is not guaranteed in the modal scenario, we suggest reading this short paper.

Each algorithm above is simply a small wrapper around anchored_semantics:

Utilities

The following utilities often involve performing some combinatoric trick between Itemsets and ARules, and might be useful to avoid reinventing the wheel.

These are three common types definition appearing during modal association rule mining.

const WorldMask = BitVector

const EnhancedItemset = Tuple{Itemset,UInt32}

const ConditionalPatternBase = Vector{EnhancedItemset}

We can enrich the MiningState of an AbstractMiner by using the following trait, depending on the specific algorithm and the kind of data we want to handle.