Skip to content

Commit

Permalink
Add truthsupertype, adjust TruthDict
Browse files Browse the repository at this point in the history
  • Loading branch information
@giopaglia
giopaglia committed Nov 5, 2023
1 parent e42396f commit f60040b
Show file tree
Hide file tree
Showing 5 changed files with 98 additions and 94 deletions.
23 changes: 13 additions & 10 deletions src/base-logic.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,10 @@ See also [`Bot`](@ref), [`Top`](@ref), [`BooleanAlgebra`](@ref).
"""
abstract type BooleanTruth <: Truth end

function Base.show(io::IO, φ::BooleanTruth)
print(io, "$(syntaxstring(φ))")
end

doc_TOP = """
struct Top <: Truth end
const TOP = Top()
Expand All @@ -222,6 +226,7 @@ const ⊤ = TOP
syntaxstring(o::Top; kwargs...) = "⊤"

istop(t::Top) = true
truthsupertype(T::Type{Top}) = BooleanTruth

doc_BOTTOM = """
struct Bot <: Truth end
Expand All @@ -243,6 +248,7 @@ const ⊥ = BOT
syntaxstring(o::Bot; kwargs...) = "⊥"

isbot(t::Bot) = true
truthsupertype(T::Type{Bot}) = BooleanTruth

# NOTE: it could be useful to provide a macro to easily create
# a new set of Truth types. In particular, a new subtree of types must be planted
Expand All @@ -253,10 +259,10 @@ Base.promote_rule(::Type{<:BooleanTruth}, ::Type{<:BooleanTruth}) = BooleanTruth
Base.convert(::Type{Bool}, ::Top) = true
Base.convert(::Type{Bool}, ::Bot) = false

function Base.convert(::Type{<:BooleanTruth}, t::Bool)::BooleanTruth
function Base.convert(::Type{BooleanTruth}, t::Bool)::BooleanTruth
return (t ? TOP : BOT)
end
function Base.convert(::Type{<:BooleanTruth}, t::Integer)::BooleanTruth
function Base.convert(::Type{BooleanTruth}, t::Integer)::BooleanTruth
if isone(t)
return TOP
elseif iszero(t)
Expand All @@ -265,12 +271,9 @@ function Base.convert(::Type{<:BooleanTruth}, t::Integer)::BooleanTruth
return error("Cannot interpret Integer value $t as BooleanTruth.")
end
end
function Base.convert(
::Type{<:BooleanTruth},
::Type{T}
)::BooleanTruth where {T<:BooleanTruth}
return T
end

Base.convert(::Type{Truth}, t::Bool) = Base.convert(BooleanTruth, t)
Base.convert(::Type{Truth}, t::Integer) = Base.convert(BooleanTruth, t)

# NOTE: are these useful?
hasdual(::typeof(⊤)) = true
Expand Down Expand Up @@ -300,8 +303,8 @@ bot(::BooleanAlgebra) = BOT

function collatetruth(
c::Connective,
ch::NTuple{N,T}
)::BooleanTruth where {N,T<:BooleanTruth}
ch::NTuple{N,T where T<:BooleanTruth}
)::BooleanTruth where {N}
_collatetruth(c, convert.(Bool, ch)) == true ? TOP : BOT
end

Expand Down
115 changes: 58 additions & 57 deletions src/core.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -526,12 +526,17 @@ See also [`istop`](@ref), [`Truth`](@ref).
"""
isbot(t::Truth)::Bool = false

function Base.convert(::Type{Truth}, t::Bool)
error("Please, provide method convert(::Type{Truth}, t::$(typeof(t))).")
end
function Base.convert(::Type{Truth}, t::Integer)
error("Please, provide method convert(::Type{Truth}, t::$(typeof(t))).")
"""
truthsupertype(T::Type{<:Truth})::Type
Return the supertype of a `Truth` type that includes all values of the same algebra.
See also [`Truth`](@ref), [`TruthDict`](@ref).
"""
function truthsupertype(T::Type{<:Truth})
return T
end

function Base.convert(::Type{Truth}, t)::Truth
return error("Cannot interpret value $t of type ($(typeof(t))) as Truth.")
end
Expand Down Expand Up @@ -585,12 +590,6 @@ function (op::Operator)(children::NTuple{N,Formula}) where {N}
T = Base.promote_type((typeof.(children))...)
T <: SyntaxTree || (children = Base.promote(children...))
return joinformulas(op, children)
# TODO remove this?
# return joinformulas(op, tree.(children))
# return joinformulas(op, Base.promote(children...))
# println(typeof.(children))
# println(typeof.(Base.promote(children...)))
# println(typeof.(children))
end

############################################################################################
Expand Down Expand Up @@ -774,31 +773,27 @@ valuetype(::AbstractInterpretation{A,T}) where {A,T} = A
truthtype(::AbstractInterpretation{A,T}) where {A,T} = T

############################################################################################
#### Check & Interpret #####################################################################
#### Interpret & Check #####################################################################
############################################################################################

"""
check(
interpret(
φ::Formula,
i::AbstractInterpretation,
args...;
kwargs...
)::Bool
)::Formula
Check a formula on a logical interpretation (or model), returning `true` if the truth value
for the formula `istop`.
This process is referred to as (finite)
[model checking](https://en.wikipedia.org/wiki/Model_checking), and there are many
algorithms for it, typically depending on the complexity of the logic.
Return the truth value for a formula on a logical interpretation (or model).
# Examples
```jldoctest
julia> @atoms String p q
julia> @atoms p q
2-element Vector{Atom{String}}:
Atom{String}("p")
Atom{String}("q")
p
q
julia> td = TruthDict([p => TOP, q => BOT])
julia> td = TruthDict([p => true, q => false])
TruthDict with values:
┌────────┬────────┐
│ q │ p │
Expand All @@ -807,74 +802,80 @@ TruthDict with values:
│ ⊥ │ ⊤ │
└────────┴────────┘
julia> check(CONJUNCTION(p,q), td)
false
julia> interpret(CONJUNCTION(p,q), td)
⊥
```
See also [`interpret`](@ref), [`Formula`](@ref), [`AbstractInterpretation`](@ref),
[`TruthDict`](@ref).
See also [`check`](@ref), [`Formula`](@ref), [`AbstractInterpretation`](@ref),
[`AbstractAlgebra`](@ref).
"""
function check(
function interpret(
φ::Formula,
i::AbstractInterpretation,
args...;
kwargs...
)::Bool
istop(interpret(φ, i, args...; kwargs...))
)::Formula
interpret(tree(φ), i, args...; kwargs...)
end

function interpret(
φ::SyntaxBranch,
i::AbstractInterpretation,
args...;
kwargs...
)::Formula
return error("Please, provide method " *
"interpret(φ::SyntaxBranch, i::$(typeof(i)), " *
"args...::$(typeof(args)); " *
"kwargs...::$(typeof(kwargs))::$(truthtype(i)).")
end

interpret(t::Truth, i::AbstractInterpretation, args...; kwargs...) = t

"""
interpret(
check(
φ::Formula,
i::AbstractInterpretation,
args...;
kwargs...
)::Formula
)::Bool
Return the truth value for a formula on a logical interpretation (or model).
Check a formula on a logical interpretation (or model), returning `true` if the truth value
for the formula `istop`.
This process is referred to as (finite)
[model checking](https://en.wikipedia.org/wiki/Model_checking), and there are many
algorithms for it, typically depending on the complexity of the logic.
# Examples
```jldoctest
julia> @atoms p q
julia> @atoms String p q
2-element Vector{Atom{String}}:
p
q
Atom{String}("p")
Atom{String}("q")
julia> td = TruthDict([p => true, q => false])
julia> td = TruthDict([p => TOP, q => BOT])
TruthDict with values:
┌────────┬────────┐
│ q │ p │
│ String │ String │
├────────┼────────┤
│ Bot: ⊥ │ Top: ⊤ │
│ ⊥ │ ⊤ │
└────────┴────────┘
julia> interpret(CONJUNCTION(p,q), td)
⊥
julia> check(CONJUNCTION(p,q), td)
false
```
See also [`check`](@ref), [`Formula`](@ref), [`AbstractInterpretation`](@ref),
[`AbstractAlgebra`](@ref).
See also [`interpret`](@ref), [`Formula`](@ref), [`AbstractInterpretation`](@ref),
[`TruthDict`](@ref).
"""
function interpret(
function check(
φ::Formula,
i::AbstractInterpretation,
args...;
kwargs...
)::Formula
interpret(tree(φ), i, args...; kwargs...)
end

function interpret(
φ::SyntaxBranch,
i::AbstractInterpretation,
args...;
kwargs...
)::Formula
return error("Please, provide method " *
"interpret(φ::SyntaxBranch, i::$(typeof(i)), " *
"args...::$(typeof(args)); " *
"kwargs...::$(typeof(kwargs))::$(truthtype(i)).")
)::Bool
istop(interpret(φ, i, args...; kwargs...))
end

############################################################################################
Expand Down
34 changes: 13 additions & 21 deletions src/propositional-logic.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,17 +153,6 @@ function interpret(
end
end

interpret(t::Truth, args...; kwargs...) = t

# Different ways to call interpret
# i[a] -> (a itself, or a single Truth value!)
# This has to be user-defined when creating a custom AbstractAssignment concrete type.
# Otherwise, an error is thrown noticing the user (see our most general dispatch).
# Note by Gio: these are written for AbstractAssignment, but
# isn't this true for any AbstractInterpretation? That is, also at the non-propositional level?
# Probably. Therefore, these should be moved to core and AbstractAssignment->AbstractInterpretation.
# By Mauro: Done, see core.jl after AbstractInterpretation definition

############################################################################################
#################################### IMPLEMENTATIONS #######################################
############################################################################################
Expand All @@ -188,7 +177,7 @@ TruthDict with values:
│ 4 │ 2 │ 3 │ 1 │
│ Int64 │ Int64 │ Int64 │ Int64 │
├────────┼────────┼────────┼────────┤
│ Top: ⊤ │ Top: ⊤ │ Top: ⊤ │ Top: ⊤ │
│ ⊤ │ ⊤ │ ⊤ │ ⊤ │
└────────┴────────┴────────┴────────┘
Expand Down Expand Up @@ -218,7 +207,9 @@ true
!!! note
If prompted for the value of an unknown atom, this throws an error.
If not specified, `BooleanTruth`s is the default `Truth` value type.
If boolean, integer, or float values are specified, they are converted to
`Truth` values.
If the structure is initialized as empty, `BooleanTruth` values are assumed.
See also
[`DefaultedTruthDict`](@ref),
Expand All @@ -239,13 +230,13 @@ struct TruthDict{
T<:Truth,
D<:AbstractDict{<:Atom{<:A},T},
}
# If the truth dict only contains a Top, then we want to upcast the dictionary
# to contain the whole BooleanTruth group.
# If T is already BooleanTruth, for example, then we want to keep it as is.
truthtype = isconcretetype(T) ? supertype(T) : T
d = Dict{Atom{A},truthtype}(d)
# Example:
# If the truth dict only contains a `Top`, then we want to upcast the dictionary
# to expect `BooleanTruth`, not only `Top`'s.
_T = truthsupertype(T)
d = Dict{Atom{A},_T}(d)

return new{A,truthtype,typeof(d)}(d)
return new{A,_T,typeof(d)}(d)
end
function TruthDict{A,T}(d::AbstractDict{<:Atom,T}) where {A,T<:Truth}
return TruthDict{A,T,typeof(d)}(d)
Expand All @@ -266,7 +257,7 @@ struct TruthDict{
return TruthDict(Dict([(Atom{A}(a),v) for (a,v) in d]))
end
function TruthDict(d::AbstractDict)
d = Dict([(a, convert(BooleanTruth, v)) for (a,v) in d])
d = Dict([(a, convert(Truth, v)) for (a,v) in d])
return TruthDict(d)
end
function TruthDict(v::AbstractVector, truth_value = ⊤)
Expand Down Expand Up @@ -309,7 +300,8 @@ struct TruthDict{
function TruthDict{A}() where {
A,
}
return TruthDict{A,BooleanTruth}()
T = BooleanTruth
return TruthDict{A,T}()
end
function TruthDict()
A = Any
Expand Down
2 changes: 1 addition & 1 deletion src/syntax-utils.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ struct LeftmostLinearForm{C<:Connective,SS<:AbstractSyntaxStructure} <: Abstract
function LeftmostLinearForm{C,SS}(
children::Vector,
) where {C<:Connective,SS<:AbstractSyntaxStructure}
a = arity(C)
a = arity(C()) # TODO maybe add member connective::C and use that instead of C()
n_children = length(children)

if a == 0
Expand Down
18 changes: 13 additions & 5 deletions test/core.jl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -200,19 +200,23 @@ f_conj_int = @test_nowarn CONJUNCTION(f_int, f_int, f_int)
@test_nowarn TruthDict()
@test_nowarn TruthDict([])
@test_throws ErrorException TruthDict((2,3),)
@test_nowarn TruthDict((2,0),)
@test_nowarn TruthDict((2,true),)
@test_nowarn TruthDict((p1, true),)
@test_nowarn TruthDict([(p1, true),])
@test_nowarn TruthDict(p1 => true)
@test_nowarn TruthDict([p1 => true])
@test_nowarn TruthDict(Dict([p1 => true]))

anch_φ_int = f_int(p1 ∧ p100 → p2)
anch_φ_int = f_int(p1 ∧ p100 ∧ p2)
anch2_φ_int = f_int(p1 ∧ p100 → p2)

for i in 1:10
_tdict = TruthDict(Dict([p => rand([true, false]) for p in unique(atoms(anch_φ_int))]))
check(anch_φ_int, _tdict) && @test all(collect(values(_tdict.truth)))
!check(anch_φ_int, _tdict) && @test !all(collect(values(_tdict.truth)))
# i == 1 && println(_tdict)
check(anch_φ_int, _tdict) && @test all(istop, collect(values(_tdict.truth)))
!check(anch_φ_int, _tdict) && @test !all(istop, collect(values(_tdict.truth)))
check(anch2_φ_int, _tdict)
end

tdict = TruthDict(Dict([p => true for p in unique(atoms(anch_φ_int))]))
Expand All @@ -229,8 +233,12 @@ tdict = TruthDict(Dict([p => false for p in unique(atoms(anch_φ_int))]))

for i in 1:10
_tdict = TruthDict(Dict([p => rand([true, false]) for p in unique(atoms(φ_int))]))
check(φ_int, _tdict) && @test all(collect(values(_tdict.truth)))
!check(φ_int, _tdict) && @test !all(collect(values(_tdict.truth)))
check(φ_int, _tdict) && @test all(istop, collect(values(_tdict.truth)))
!check(φ_int, _tdict) && @test !all(istop, collect(values(_tdict.truth)))

@test_nowarn _tdict[φ_int]
@test_nowarn φ_int(_tdict)
@test φ_int(_tdict) == _tdict[φ_int]
end

tdict = TruthDict(Dict([p => true for p in unique(atoms(φ_int))]))
Expand Down

0 comments on commit f60040b

Please sign in to comment.