diff --git a/dev/.documenter-siteinfo.json b/dev/.documenter-siteinfo.json index 5a3d02b..4136e6e 100644 --- a/dev/.documenter-siteinfo.json +++ b/dev/.documenter-siteinfo.json @@ -1 +1 @@ -{"documenter":{"julia_version":"1.9.4","generation_timestamp":"2024-07-05T11:06:15","documenter_version":"1.5.0"}} \ No newline at end of file +{"documenter":{"julia_version":"1.9.4","generation_timestamp":"2024-07-05T11:06:22","documenter_version":"1.5.0"}} \ No newline at end of file diff --git a/dev/index.html b/dev/index.html index 9959d73..f115482 100644 --- a/dev/index.html +++ b/dev/index.html @@ -1,5 +1,5 @@ -Home · SoleData.jl
GitHub

SoleData

Welcome to the documentation for SoleData.

Logical foundations

See SoleLogics for more.

SoleLogics.Atom — Type
struct Atom{V} <: SyntaxLeaf
+Home · SoleData.jl
GitHub
SoleData
Welcome to the documentation for SoleData.
Logical foundations
See SoleLogics for more.
SoleLogics.Atom — Type
struct Atom{V} <: SyntaxLeaf
     value::V
 end
An atom, sometimes called an atomic proposition, propositional letter (or simply letter), of type Atom{V} wraps a value::V representing a fact which truth can be assessed on a logical interpretation.
Atoms are nullary tokens (i.e, they are at the leaves of a syntax tree); note that their atoms cannot be Atoms.
See also AbstractInterpretation, atoms, check, SyntaxToken.
source
SoleLogics.AbstractWorld — Type
abstract type AbstractWorld end
Abstract type for the nodes of an annotated accessibility graph (Kripke structure). This is used, for example, in modal logic, where the truth of formulas is relativized to worlds, that is, nodes of a graph.
Implementing
When implementing a new world type, the logical semantics should be defined via accessibles methods; refer to the help for accessibles.
See also AbstractKripkeStructure, AbstractFrame.
source
SoleData.minify — Function
minify(dataset::D1)::Tuple{D2,Function} where {D1,D2}
Return a minified version of a dataset, as well as a backmap for reverting to the original dataset. Dataset minification remaps each scalar values in the dataset to a new value such that the overall order of the values is preserved; the output dataset is smaller in size, since it relies on values of type UInt8, UInt16, UInt32, etc.
See also isminifiable.
source
Logisets
SoleData.minify — Function
minify(dataset::D1)::Tuple{D2,Function} where {D1,D2}
Return a minified version of a dataset, as well as a backmap for reverting to the original dataset. Dataset minification remaps each scalar values in the dataset to a new value such that the overall order of the values is preserved; the output dataset is smaller in size, since it relies on values of type UInt8, UInt16, UInt32, etc.
See also isminifiable.
source
Logisets
SoleData.Feature — Type
struct Feature{A} <: AbstractFeature
     atom::A
-end
A feature solely identified by an atom (e.g., a string with its name, a tuple of strings, etc.)
See also AbstractFeature.
source
SoleData.MultivariateFeature — Type
struct MultivariateFeature{U} <: VarFeature
     f::Function
-end
A dimensional feature represented by the application of a function to a dimensional channel. For example, it can wrap a scalar function computing how much a Interval2D world, when interpreted on an image, resembles a horse. Note that the image has a number of spatial variables (3, for the case of RGB), and "resembling a horse" may require a computation involving all variables.
See also SoleLogics.Interval, SoleLogics.Interval2D, AbstractUnivariateFeature, VarFeature, AbstractFeature.
source
SoleData.UnivariateFeature — Type
struct UnivariateFeature{U} <: AbstractUnivariateFeature
+end
A dimensional feature represented by the application of a function to a dimensional channel. For example, it can wrap a scalar function computing how much a Interval2D world, when interpreted on an image, resembles a horse. Note that the image has a number of spatial variables (3, for the case of RGB), and "resembling a horse" may require a computation involving all variables.
See also SoleLogics.Interval, SoleLogics.Interval2D, AbstractUnivariateFeature, VarFeature, AbstractFeature.
source
SoleData.VarFeature — Type
abstract type VarFeature <: AbstractFeature end
Abstract type for feature functions that can be computed on (multi)variate data. Instances of multivariate datasets have values for a number of variables, which can be used to define logical features.
For example, with dimensional data (e.g., multivariate time series, digital images and videos), features can be computed as the minimum value for a given variable on a specific interval/rectangle/cuboid (in general, a `SoleLogics.GeometricalWorld).
As an example of a dimensional feature, consider min[V1], which computes the minimum for variable 1 for a given world. ScalarConditions such as min[V1] >= 10 can be, then, evaluated on worlds.
See also scalarlogiset, featvaltype, computefeature, SoleLogics.Interval.
source
SoleData.VarFeature — Type
abstract type VarFeature <: AbstractFeature end
Abstract type for feature functions that can be computed on (multi)variate data. Instances of multivariate datasets have values for a number of variables, which can be used to define logical features.
For example, with dimensional data (e.g., multivariate time series, digital images and videos), features can be computed as the minimum value for a given variable on a specific interval/rectangle/cuboid (in general, a `SoleLogics.GeometricalWorld).
As an example of a dimensional feature, consider min[V1], which computes the minimum for variable 1 for a given world. ScalarConditions such as min[V1] >= 10 can be, then, evaluated on worlds.
See also scalarlogiset, featvaltype, computefeature, SoleLogics.Interval.
source
SoleData.parsefeature — Method
parsefeature(FT::Type{<:AbstractFeature}, expr::String; kwargs...)
Parse a feature of type FT from its syntaxstring representation. Depending on FT, specifying keyword arguments such as featvaltype::Type may be required or recommended.
See also parsecondition.
source
SoleData.parsefeature — Method
parsefeature(FT::Type{<:VarFeature}, expr::String; kwargs...)
Parse a VarFeature of type FT from its syntaxstring representation.
Keyword Arguments
  • featvaltype::Union{Nothing,Type} = nothing: the feature's featvaltype   (recommended for some features, e.g., UnivariateFeature);
  • opening_parenthesis::String = "[":   the string signaling the opening of an expression block (e.g., "min[V2]");
  • closing_parenthesis::String = "]":   the string signaling the closing of an expression block (e.g., "min[V2]");
  • additional_feature_aliases = Dict{String,Base.Callable}(): A dictionary mapping strings to   callables, useful when parsing custom-made, non-standard features.   By default, features such as "avg" or "min" are provided for   (see SoleData.BASE_FEATURE_FUNCTIONS_ALIASES);   note that, in case of clashing strings,   the provided additional aliases will override the standard ones;
  • variable_names_map::Union{Nothing,AbstractDict,AbstractVector} = nothing:   mapping from variable name to variable index, useful when parsing from   syntaxstrings with variable names (e.g., "min[Heart rate]");
  • variable_name_prefix::String = "V":   prefix used with variable indices (e.g., "V10").
Note that at most one argument in variable_names_map and variable_name_prefix should be provided.
Note
The default parentheses, here, differ from those of `SoleLogics.parseformula, since features are typically wrapped into Atoms, and parseformula does not allow parenthesis characters in atoms' syntaxstrings.
See also VarFeature, featvaltype, parsecondition.
source
SoleData.parsefeature — Method
parsefeature(FT::Type{<:AbstractFeature}, expr::String; kwargs...)
Parse a feature of type FT from its syntaxstring representation. Depending on FT, specifying keyword arguments such as featvaltype::Type may be required or recommended.
See also parsecondition.
source
SoleData.parsefeature — Method
parsefeature(FT::Type{<:VarFeature}, expr::String; kwargs...)
Parse a VarFeature of type FT from its syntaxstring representation.
Keyword Arguments
  • featvaltype::Union{Nothing,Type} = nothing: the feature's featvaltype   (recommended for some features, e.g., UnivariateFeature);
  • opening_parenthesis::String = "[":   the string signaling the opening of an expression block (e.g., "min[V2]");
  • closing_parenthesis::String = "]":   the string signaling the closing of an expression block (e.g., "min[V2]");
  • additional_feature_aliases = Dict{String,Base.Callable}(): A dictionary mapping strings to   callables, useful when parsing custom-made, non-standard features.   By default, features such as "avg" or "min" are provided for   (see SoleData.BASE_FEATURE_FUNCTIONS_ALIASES);   note that, in case of clashing strings,   the provided additional aliases will override the standard ones;
  • variable_names_map::Union{Nothing,AbstractDict,AbstractVector} = nothing:   mapping from variable name to variable index, useful when parsing from   syntaxstrings with variable names (e.g., "min[Heart rate]");
  • variable_name_prefix::String = "V":   prefix used with variable indices (e.g., "V10").
Note that at most one argument in variable_names_map and variable_name_prefix should be provided.
Note
The default parentheses, here, differ from those of `SoleLogics.parseformula, since features are typically wrapped into Atoms, and parseformula does not allow parenthesis characters in atoms' syntaxstrings.
See also VarFeature, featvaltype, parsecondition.
source
SoleData.variable_name — Method
variable_name(
     f::AbstractUnivariateFeature;
     variable_names_map::Union{Nothing,AbstractDict,AbstractVector} = nothing,
     variable_name_prefix::Union{Nothing,String} = "V",
-)::String
Return the name of the variable targeted by a univariate feature. By default, an variable name is a number prefixed by "V"; however, variable_names_map or variable_name_prefix can be used to customize variable names. The prefix can be customized by specifying variable_name_prefix. Alternatively, a mapping from string to integer (either via a Dictionary or a Vector) can be passed as variable_names_map. Note that only one in variable_names_map and variable_name_prefix should be provided.
See also parsecondition, ScalarCondition, syntaxstring.
source
SoleData.FunctionalCondition — Type
struct FunctionalCondition{FT<:AbstractFeature} <: AbstractCondition{FT}
+)::String
Return the name of the variable targeted by a univariate feature. By default, an variable name is a number prefixed by "V"; however, variable_names_map or variable_name_prefix can be used to customize variable names. The prefix can be customized by specifying variable_name_prefix. Alternatively, a mapping from string to integer (either via a Dictionary or a Vector) can be passed as variable_names_map. Note that only one in variable_names_map and variable_name_prefix should be provided.
See also parsecondition, ScalarCondition, syntaxstring.
source
SoleData.ScalarCondition — Type
struct ScalarCondition{U,FT<:AbstractFeature,M<:ScalarMetaCondition{FT}} <: AbstractCondition{FT}
+end
A condition which yields a truth value equal to the value of a function.
See also AbstractFeature.
source
SoleData.ScalarCondition — Type
struct ScalarCondition{U,FT<:AbstractFeature,M<:ScalarMetaCondition{FT}} <: AbstractCondition{FT}
     metacond::M
     a::U
-end
A scalar condition comparing a computed feature value (see ScalarMetaCondition) and a threshold value a. It can be evaluated on a world of an instance of a logical dataset.
For example: $min[V1] ≥ 10$, which translates to "Within this world, the minimum of variable 1 is greater or equal than 10." In this case, the feature a VariableMin object.
See also AbstractCondition, ScalarMetaCondition.
source
SoleData.ScalarMetaCondition — Type
struct ScalarMetaCondition{FT<:AbstractFeature,O<:TestOperator} <: AbstractCondition{FT}
+end
A scalar condition comparing a computed feature value (see ScalarMetaCondition) and a threshold value a. It can be evaluated on a world of an instance of a logical dataset.
For example: $min[V1] ≥ 10$, which translates to "Within this world, the minimum of variable 1 is greater or equal than 10." In this case, the feature a VariableMin object.
See also AbstractCondition, ScalarMetaCondition.
source
SoleData.ScalarMetaCondition — Type
struct ScalarMetaCondition{FT<:AbstractFeature,O<:TestOperator} <: AbstractCondition{FT}
     feature::FT
     test_operator::O
-end
A metacondition representing a scalar comparison method. Here, the feature is a scalar function that can be computed on a world of an instance of a logical dataset. A test operator is a binary mathematical relation, comparing the computed feature value and an external threshold value (see ScalarCondition). A metacondition can also be used for representing the infinite set of conditions that arise with a free threshold (see UnboundedScalarAlphabet): ${min[V1] ≥ a, a ∈ ℝ}$.
See also AbstractCondition, ScalarCondition.
source
SoleData.UnivariateScalarAlphabet — Type
struct UnivariateScalarAlphabet <: AbstractAlphabet{ScalarCondition}
+end
A metacondition representing a scalar comparison method. Here, the feature is a scalar function that can be computed on a world of an instance of a logical dataset. A test operator is a binary mathematical relation, comparing the computed feature value and an external threshold value (see ScalarCondition). A metacondition can also be used for representing the infinite set of conditions that arise with a free threshold (see UnboundedScalarAlphabet): ${min[V1] ≥ a, a ∈ ℝ}$.
See also AbstractCondition, ScalarCondition.
source
SoleData.parsecondition — Method
parsecondition(C::Type{<:AbstractCondition}, expr::String; kwargs...)
Parse a condition of type C from its syntaxstring representation. Depending on C, specifying keyword arguments such as featuretype::Type{<:AbstractFeature}, and featvaltype::Type may be required or recommended.
See also parsefeature.
source
SoleData.parsecondition — Method
parsecondition(C::Type{<:AbstractCondition}, expr::String; kwargs...)
Parse a condition of type C from its syntaxstring representation. Depending on C, specifying keyword arguments such as featuretype::Type{<:AbstractFeature}, and featvaltype::Type may be required or recommended.
See also parsefeature.
source
SoleData.representatives — Method
representatives(
     fr::AbstractFrame{W},
     S::W,
     ::AbstractRelation,
     ::AbstractCondition
-) where {W<:AbstractWorld}
Return an iterator to the (few) representative accessible worlds that are necessary for computing and propagating truth values through existential modal connectives. When this optimization is possible (e.g., when checking specific formulas on scalar conditions), it allows to further boost "one-step" optimizations (see AbstractOneStepMemoset).
For example, consider a Kripke structure with a 1-dimensional FullDimensionalFrame of length 100, and the problem of checking a formula "⟨L⟩(max[V1] ≥ 10)" on a SoleLogics.Interval SoleLogics.Interval{Int64}(1, 2) (with L being Allen's "Later" relation, see SoleLogics.IA_L). Comparing 10 with the (maximum) "max[V1]" computed on all worlds is the naïve strategy to check the formula. However, in this case, comparing 10 to the "max[V1]" computed on the single Interval SoleLogics.Interval{Int64}(2, 101) suffice to establish whether the structure satisfies the formula. Similar cases arise depending on the relation, feature and test operator (or, better, its aggregator).
Note that this method fallsback to accessibles.
See also SoleLogics.accessibles, ScalarCondition, SoleLogics.AbstractFrame.
source
SoleData.MultiFormula — Type
struct MultiFormula{F<:Formula} <: AbstractSyntaxStructure
+) where {W<:AbstractWorld}
Return an iterator to the (few) representative accessible worlds that are necessary for computing and propagating truth values through existential modal connectives. When this optimization is possible (e.g., when checking specific formulas on scalar conditions), it allows to further boost "one-step" optimizations (see AbstractOneStepMemoset).
For example, consider a Kripke structure with a 1-dimensional FullDimensionalFrame of length 100, and the problem of checking a formula "⟨L⟩(max[V1] ≥ 10)" on a SoleLogics.Interval SoleLogics.Interval{Int64}(1, 2) (with L being Allen's "Later" relation, see SoleLogics.IA_L). Comparing 10 with the (maximum) "max[V1]" computed on all worlds is the naïve strategy to check the formula. However, in this case, comparing 10 to the "max[V1]" computed on the single Interval SoleLogics.Interval{Int64}(2, 101) suffice to establish whether the structure satisfies the formula. Similar cases arise depending on the relation, feature and test operator (or, better, its aggregator).
Note that this method fallsback to accessibles.
See also SoleLogics.accessibles, ScalarCondition, SoleLogics.AbstractFrame.
source
SoleData.MultiFormula — Type
struct MultiFormula{F<:Formula} <: AbstractSyntaxStructure
     modforms::Dict{Int,F}
-end
A symbolic antecedent that can be checked on a MultiLogiset, associating antecedents to modalities.
source
SoleData.MultiLogiset — Type
struct MultiLogiset{L<:AbstractLogiset}
+end
A symbolic antecedent that can be checked on a MultiLogiset, associating antecedents to modalities.
source
SoleData.PropositionalLogiset — Type
PropositionalLogiset(table)
A logiset of propositional interpretations, wrapping a Tables' table of real/string/categorical values.
Examples
This structure can be used to check propositional formulas:
using SoleData, MLJBase
+end
A logical dataset composed of different modalities); this structure is useful for representing multimodal datasets in logical terms.
See also AbstractLogiset, minify.
source
SoleData.PropositionalLogiset — Type
PropositionalLogiset(table)
A logiset of propositional interpretations, wrapping a Tables' table of real/string/categorical values.
Examples
This structure can be used to check propositional formulas:
using SoleData, MLJBase
 
 X = PropositionalLogiset(MLJBase.load_iris())
 
@@ -163,24 +163,24 @@
 satmask = check(φ, X) # Check the formula on the whole dataset
 
 slicedataset(X, satmask)
-slicedataset(X, (!).(satmask))
See also AbstractLogiset, AbstractAssignment.
source
SoleLogics.alphabet — Function
alphabet(X::PropositionalLogiset, sorted=true;
          test_operators::Union{Nothing,AbstractVector{<:TestOperator},Base.Callable}=nothing,
          discretizedomain=false, y::Union{Nothing, AbstractVector}=nothing
-)::UnionAlphabet{ScalarCondition,UnivariateScalarAlphabet}
Constructs an alphabet based on the provided PropositionalLogiset X, with optional parameters:
  • sorted: whether to sort the atoms in the sub-alphabets (i.e., the threshold domains),   by a truer-first policy (default: true)
  • test_operators: test operators to use (defaulted to [≤, ≥] for real-valued features, and [(==), (≠)] for other features, e.g., categorical)
  • discretizedomain: whether to discretize the domain (default: false)
  • y: vector used for discretization (required if discretizedomain is true)
Returns a UnionAlphabet containing ScalarCondition and UnivariateScalarAlphabet.
source
SoleData.AbstractMemoset — Type
abstract type AbstractMemoset{
+)::UnionAlphabet{ScalarCondition,UnivariateScalarAlphabet}
Constructs an alphabet based on the provided PropositionalLogiset X, with optional parameters:
  • sorted: whether to sort the atoms in the sub-alphabets (i.e., the threshold domains),   by a truer-first policy (default: true)
  • test_operators: test operators to use (defaulted to [≤, ≥] for real-valued features, and [(==), (≠)] for other features, e.g., categorical)
  • discretizedomain: whether to discretize the domain (default: false)
  • y: vector used for discretization (required if discretizedomain is true)
Returns a UnionAlphabet containing ScalarCondition and UnivariateScalarAlphabet.
source
SoleData.AbstractModalLogiset — Type
abstract type AbstractModalLogiset{
     W<:AbstractWorld,
     U,
     FT<:AbstractFeature,
     FR<:AbstractFrame{W},
-} <: AbstractLogiset end
Abstract type for logisets, that is, logical datasets for symbolic learning where each instance is a Kripke structure associating feature values to each world. Conditions (see AbstractCondition), and logical formulas with conditional letters can be checked on worlds of instances of the dataset.
See also AbstractCondition, AbstractFeature, SoleLogics.AbstractKripkeStructure, SoleLogics.AbstractInterpretationSet.
source
SoleData.ScalarOneStepMemoset — Type
One-step memoization structures for optimized check of formulas of type ⟨R⟩p, where p wraps a scalar condition, such as MyFeature ≥ 10. With such formulas, scalar one-step optimization can be performed.
For example, checking ⟨R⟩(MyFeature ≥ 10) on a world w of a Kripke structure involves comparing the maximum MyFeature across ws accessible worlds with 10; but the same maximum value can be reused to check sibling formulas such as ⟨R⟩(MyFeature ≥ 100). This sparks the idea of storing and reusing scalar aggregations (e.g., minimum/maximum) over the feature values. Each value refers to a specific world, and an object of type ⟨R⟩(f ⋈ ?), called a "scalar metacondition".
Similar cases arise depending on the relation and the test operator (or, better, its aggregator), and further optimizations can be applied for specific feature types (see representatives).
An immediate special case, however, arises when R is the global relation G since, in such case, a single aggregate value is enough for all worlds within the Kripke structure. Therefore, we differentiate between generic, relational memosets (see AbstractScalarOneStepRelationalMemoset), and global memosets (see AbstractScalarOneStepGlobalMemoset), which are usually much smaller.
Given a logiset X, a ScalarOneStepMemoset covers a set of relations and metaconditions, and it holds both a relational and a global memoset. It can be instantiated via:
ScalarOneStepMemoset(
+} <: AbstractLogiset end
Abstract type for logisets, that is, logical datasets for symbolic learning where each instance is a Kripke structure associating feature values to each world. Conditions (see AbstractCondition), and logical formulas with conditional letters can be checked on worlds of instances of the dataset.
See also AbstractCondition, AbstractFeature, SoleLogics.AbstractKripkeStructure, SoleLogics.AbstractInterpretationSet.
source
SoleData.ScalarOneStepMemoset — Type
One-step memoization structures for optimized check of formulas of type ⟨R⟩p, where p wraps a scalar condition, such as MyFeature ≥ 10. With such formulas, scalar one-step optimization can be performed.
For example, checking ⟨R⟩(MyFeature ≥ 10) on a world w of a Kripke structure involves comparing the maximum MyFeature across ws accessible worlds with 10; but the same maximum value can be reused to check sibling formulas such as ⟨R⟩(MyFeature ≥ 100). This sparks the idea of storing and reusing scalar aggregations (e.g., minimum/maximum) over the feature values. Each value refers to a specific world, and an object of type ⟨R⟩(f ⋈ ?), called a "scalar metacondition".
Similar cases arise depending on the relation and the test operator (or, better, its aggregator), and further optimizations can be applied for specific feature types (see representatives).
An immediate special case, however, arises when R is the global relation G since, in such case, a single aggregate value is enough for all worlds within the Kripke structure. Therefore, we differentiate between generic, relational memosets (see AbstractScalarOneStepRelationalMemoset), and global memosets (see AbstractScalarOneStepGlobalMemoset), which are usually much smaller.
Given a logiset X, a ScalarOneStepMemoset covers a set of relations and metaconditions, and it holds both a relational and a global memoset. It can be instantiated via:
ScalarOneStepMemoset(
     X                       :: AbstractModalLogiset{W,U},
     metaconditions          :: AbstractVector{<:ScalarMetaCondition},
     relations               :: AbstractVector{<:AbstractRelation};
     precompute_globmemoset  :: Bool = true,
     precompute_relmemoset   :: Bool = false,
     print_progress          :: Bool = false,
-)
If precompute_relmemoset is false, then the relational memoset is simply initialized as an empty structure, and memoization is performed on it upon checking formulas. precompute_globmemoset works similarly.
See SupportedLogiset, ScalarMetaCondition, AbstractOneStepMemoset.
source
Scalar Logisets
Scalar Dimensional Logisets
Multimodal Logisets

+)

If precompute_relmemoset is false, then the relational memoset is simply initialized as an empty structure, and memoization is performed on it upon checking formulas. precompute_globmemoset works similarly.

See SupportedLogiset, ScalarMetaCondition, AbstractOneStepMemoset.

source

Scalar Logisets

Scalar Dimensional Logisets

Multimodal Logisets

diff --git a/dev/objects.inv b/dev/objects.inv index 1e430f4..de09240 100644 --- a/dev/objects.inv +++ b/dev/objects.inv @@ -1,6 +1,6 @@ # Sphinx inventory version 2 # Project: SoleData.jl -# Version: 0.15.0 +# Version: 0.15.1 # The remainder of this file is compressed using zlib. xWMo0+"r+U=TBh+vrD&Wu⿯')%~3