diff --git a/.JuliaFormatter.toml b/.JuliaFormatter.toml new file mode 100644 index 00000000..580b7511 --- /dev/null +++ b/.JuliaFormatter.toml @@ -0,0 +1 @@ +style = "sciml" diff --git a/.cirrus.yml b/.cirrus.yml index fcbeeefb..0a3671d0 100644 --- a/.cirrus.yml +++ b/.cirrus.yml @@ -1,5 +1,5 @@ freebsd_instance: - image_family: freebsd-13-2 + image_family: freebsd-14-0 task: name: FreeBSD artifacts_cache: diff --git a/Project.toml b/Project.toml index 2f7b3405..ef005090 100644 --- a/Project.toml +++ b/Project.toml @@ -1,7 +1,7 @@ name = "SoleLogics" uuid = "b002da8f-3cb3-4d91-bbe3-2953433912b5" authors = ["Mauro MILELLA", "Giovanni PAGLIARINI", "Alberto PAPARELLA", "Eduard I. STAN"] -version = "0.7.1" +version = "0.8.0" [deps] AbstractTrees = "1520ce14-60c1-5f80-bbc7-55ef81b5835c" @@ -23,10 +23,10 @@ ThreadSafeDicts = "4239201d-c60e-5e0a-9702-85d713665ba7" AbstractTrees = "0.4" DataStructures = "0.18" Dictionaries = "0.3" +FunctionWrappers = "1" Graphs = "1.8" IterTools = "1" Lazy = "0.15" -FunctionWrappers = "1" PrettyTables = "2.2" Random = "1" Reexport = "1" @@ -38,9 +38,10 @@ julia = "1" [extras] InteractiveUtils = "b77e0a4c-d291-57a0-90e8-8db25a27a240" +BenchmarkTools = "6e4b80f9-dd63-53aa-95a3-0cdb28fa8baf" Markdown = "d6f4376e-aef5-505a-96c1-9c027394607a" PlutoUI = "7f904dfe-b85e-4ff6-b463-dae2292396a8" Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" [targets] -test = ["Test", "Markdown", "InteractiveUtils", "PlutoUI"] +test = ["Test", "Markdown", "InteractiveUtils", "PlutoUI", "BenchmarkTools"] diff --git a/docs/Manifest.toml b/docs/Manifest.toml index c9394489..b9dacafc 100644 --- a/docs/Manifest.toml +++ b/docs/Manifest.toml @@ -10,9 +10,9 @@ uuid = "a4c015fc-c6ff-483c-b24f-f7ea428134e9" version = "0.0.1" [[deps.AbstractTrees]] -git-tree-sha1 = "faa260e4cb5aba097a73fab382dd4b5819d8ec8c" +git-tree-sha1 = "2d9c9a55f9c93e8887ad391fbae72f8ef55e1177" uuid = "1520ce14-60c1-5f80-bbc7-55ef81b5835c" -version = "0.4.4" +version = "0.4.5" [[deps.ArgTools]] uuid = "0dad84c5-d112-42e6-8d28-ef12dabb789f" @@ -54,11 +54,17 @@ git-tree-sha1 = "c0216e792f518b39b22212127d4a84dc31e4e386" uuid = "da1fd8a2-8d9e-5ec2-8556-3022fb5608a2" version = "1.3.5" +[[deps.CodecZlib]] +deps = ["TranscodingStreams", "Zlib_jll"] +git-tree-sha1 = "59939d8a997469ee05c4b4944560a820f9ba0d73" +uuid = "944b1d66-785c-5afd-91f1-9de20f533193" +version = "0.7.4" + [[deps.Compat]] deps = ["TOML", "UUIDs"] -git-tree-sha1 = "75bd5b6fc5089df449b5d35fa501c846c9b6549b" +git-tree-sha1 = "c955881e3c981181362ae4088b35995446298b80" uuid = "34da2185-b29b-5c13-b0c7-acf172513d20" -version = "4.12.0" +version = "4.14.0" weakdeps = ["Dates", "LinearAlgebra"] [deps.Compat.extensions] @@ -81,9 +87,9 @@ version = "1.16.0" [[deps.DataStructures]] deps = ["Compat", "InteractiveUtils", "OrderedCollections"] -git-tree-sha1 = "ac67408d9ddf207de5cfa9a97e114352430f01ed" +git-tree-sha1 = "0f4b5d62a88d8f59003e43c25a8a90de9eb76317" uuid = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" -version = "0.18.16" +version = "0.18.18" [[deps.DataValueInterfaces]] git-tree-sha1 = "bfc1187b79289637fa0ef6d4436ebdfe6905cbd6" @@ -111,10 +117,10 @@ uuid = "ffbed154-4ef7-542d-bbb7-c09d3a79fcae" version = "0.9.3" [[deps.Documenter]] -deps = ["ANSIColoredPrinters", "AbstractTrees", "Base64", "Dates", "DocStringExtensions", "Downloads", "Git", "IOCapture", "InteractiveUtils", "JSON", "LibGit2", "Logging", "Markdown", "MarkdownAST", "Pkg", "PrecompileTools", "REPL", "RegistryInstances", "SHA", "Test", "Unicode"] -git-tree-sha1 = "2613dbec8f4748273bbe30ba71fd5cb369966bac" +deps = ["ANSIColoredPrinters", "AbstractTrees", "Base64", "CodecZlib", "Dates", "DocStringExtensions", "Downloads", "Git", "IOCapture", "InteractiveUtils", "JSON", "LibGit2", "Logging", "Markdown", "MarkdownAST", "Pkg", "PrecompileTools", "REPL", "RegistryInstances", "SHA", "TOML", "Test", "Unicode"] +git-tree-sha1 = "4a40af50e8b24333b9ec6892546d9ca5724228eb" uuid = "e30172f5-a6a5-5a46-863b-614d45cd2de4" -version = "1.2.1" +version = "1.3.0" [[deps.Downloads]] deps = ["ArgTools", "FileWatching", "LibCURL", "NetworkOptions"] @@ -146,21 +152,26 @@ version = "1.9.3" SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" +[[deps.FunctionWrappers]] +git-tree-sha1 = "d62485945ce5ae9c0c48f124a84998d755bae00e" +uuid = "069b7b12-0de2-55c6-9aab-29f3d0a68a2e" +version = "1.1.3" + [[deps.Future]] deps = ["Random"] uuid = "9fa8497b-333b-5362-9e8d-4d0656e87820" [[deps.Git]] deps = ["Git_jll"] -git-tree-sha1 = "51764e6c2e84c37055e846c516e9015b4a291c7d" +git-tree-sha1 = "04eff47b1354d702c3a85e8ab23d539bb7d5957e" uuid = "d7ba0133-e1db-5d97-8f8c-041e4b3a1eb2" -version = "1.3.0" +version = "1.3.1" [[deps.Git_jll]] deps = ["Artifacts", "Expat_jll", "JLLWrappers", "LibCURL_jll", "Libdl", "Libiconv_jll", "OpenSSL_jll", "PCRE2_jll", "Zlib_jll"] -git-tree-sha1 = "b30c473c97fcc1e1e44fab8f3e88fd1b89c9e9d1" +git-tree-sha1 = "12945451c5d0e2d0dca0724c3a8d6448b46bbdf9" uuid = "f8c6e375-362e-5223-8a59-34ff63f689eb" -version = "2.43.0+0" +version = "2.44.0+1" [[deps.Graphs]] deps = ["ArnoldiMethod", "Compat", "DataStructures", "Distributed", "Inflate", "LinearAlgebra", "Random", "SharedArrays", "SimpleTraits", "SparseArrays", "Statistics"] @@ -217,9 +228,9 @@ version = "0.21.4" [[deps.JuliaInterpreter]] deps = ["CodeTracking", "InteractiveUtils", "Random", "UUIDs"] -git-tree-sha1 = "04663b9e1eb0d0eabf76a6d0752e0dac83d53b36" +git-tree-sha1 = "7b762d81887160169ddfc93a47e5fd7a6a3e78ef" uuid = "aa1ae85d-cabe-5617-a682-6adf51b2e16a" -version = "0.9.28" +version = "0.9.29" [[deps.LaTeXStrings]] git-tree-sha1 = "50901ebc375ed41dbf8058da26f9de442febbbec" @@ -271,9 +282,9 @@ uuid = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" [[deps.LogExpFunctions]] deps = ["DocStringExtensions", "IrrationalConstants", "LinearAlgebra"] -git-tree-sha1 = "7d6dd4e9212aebaeed356de34ccf262a3cd415aa" +git-tree-sha1 = "18144f3e9cbe9b15b070288eef858f71b291ce37" uuid = "2ab3a3ac-af41-5b50-aa03-7779005ae688" -version = "0.3.26" +version = "0.3.27" [deps.LogExpFunctions.extensions] LogExpFunctionsChainRulesCoreExt = "ChainRulesCore" @@ -290,9 +301,9 @@ uuid = "56ddb016-857b-54e1-b83d-db4d58db5568" [[deps.LoweredCodeUtils]] deps = ["JuliaInterpreter"] -git-tree-sha1 = "20ce1091ba18bcdae71ad9b71ee2367796ba6c48" +git-tree-sha1 = "31e27f0b0bf0df3e3e951bfcc43fe8c730a219f6" uuid = "6f1432cf-f94c-5a45-995e-cdbf5db27b0b" -version = "2.4.4" +version = "2.4.5" [[deps.MacroTools]] deps = ["Markdown", "Random"] @@ -372,9 +383,9 @@ version = "1.2.0" [[deps.Preferences]] deps = ["TOML"] -git-tree-sha1 = "00805cd429dcb4870060ff49ef443486c262e38e" +git-tree-sha1 = "9306f6085165d270f7e3db02af26a400d580f5c6" uuid = "21216c6a-2e73-6563-6e65-726566657250" -version = "1.4.1" +version = "1.4.3" [[deps.PrettyTables]] deps = ["Crayons", "LaTeXStrings", "Markdown", "PrecompileTools", "Printf", "Reexport", "StringManipulation", "Tables"] @@ -413,9 +424,9 @@ version = "1.3.0" [[deps.Revise]] deps = ["CodeTracking", "Distributed", "FileWatching", "JuliaInterpreter", "LibGit2", "LoweredCodeUtils", "OrderedCollections", "Pkg", "REPL", "Requires", "UUIDs", "Unicode"] -git-tree-sha1 = "3fe4e5b9cdbb9bbc851c57b149e516acc07f8f72" +git-tree-sha1 = "12aa2d7593df490c407a3bbd8b86b8b515017f3e" uuid = "295af30f-e4ad-537b-8983-00126c2a3abe" -version = "3.5.13" +version = "3.5.14" [[deps.SHA]] uuid = "ea8e919c-243c-51af-8825-aaa63cd721ce" @@ -439,15 +450,17 @@ uuid = "6462fe0b-24de-5631-8697-dd941f90decc" [[deps.SoleBase]] deps = ["CategoricalArrays", "FillArrays", "IterTools", "Logging", "Random", "StatsBase"] -git-tree-sha1 = "1acbf3c233d2d494a8fd03dcb1fff5621bc5074f" +git-tree-sha1 = "878891f576af95083687f1039f33beb40d990fcf" uuid = "4475fa32-7023-44a0-aa70-4813b230e492" -version = "0.12.0" +version = "0.12.1" [[deps.SoleLogics]] -deps = ["AbstractTrees", "DataStructures", "Dictionaries", "Graphs", "IterTools", "Lazy", "PrettyTables", "Random", "Reexport", "Revise", "SoleBase", "StatsBase", "ThreadSafeDicts"] -git-tree-sha1 = "0ae255c1f522be5f8ee54e2714d036b13f57d983" +deps = ["AbstractTrees", "DataStructures", "Dictionaries", "FunctionWrappers", "Graphs", "IterTools", "Lazy", "PrettyTables", "Random", "Reexport", "Revise", "SoleBase", "StatsBase", "ThreadSafeDicts"] +git-tree-sha1 = "d1397a39e65fea01379e74a8ec99393395122ebe" +repo-rev = "many-valued-logics" +repo-url = ".." uuid = "b002da8f-3cb3-4d91-bbe3-2953433912b5" -version = "0.7.0" +version = "0.7.1" [[deps.SortingAlgorithms]] deps = ["DataStructures"] @@ -461,9 +474,9 @@ uuid = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" [[deps.StaticArrays]] deps = ["LinearAlgebra", "PrecompileTools", "Random", "StaticArraysCore"] -git-tree-sha1 = "7b0e9c14c624e435076d19aea1e5cbdec2b9ca37" +git-tree-sha1 = "bf074c045d3d5ffd956fa0a461da38a44685d6b2" uuid = "90137ffa-7385-5640-81b9-e52037218182" -version = "1.9.2" +version = "1.9.3" [deps.StaticArrays.extensions] StaticArraysChainRulesCoreExt = "ChainRulesCore" @@ -533,9 +546,18 @@ deps = ["InteractiveUtils", "Logging", "Random", "Serialization"] uuid = "8dfed614-e22c-5e08-85e1-65c5234f0b40" [[deps.ThreadSafeDicts]] -git-tree-sha1 = "53948619aafc920ab39e89942d1b6dfb2ae36532" +git-tree-sha1 = "300b753c0a786ea43fdafc26a4e50b87fb58cd50" uuid = "4239201d-c60e-5e0a-9702-85d713665ba7" -version = "0.1.4" +version = "0.1.6" + +[[deps.TranscodingStreams]] +git-tree-sha1 = "3caa21522e7efac1ba21834a03734c57b4611c7e" +uuid = "3bb67fe8-82b1-5028-8e26-92a6c54297fa" +version = "0.10.4" +weakdeps = ["Random", "Test"] + + [deps.TranscodingStreams.extensions] + TestExt = ["Test", "Random"] [[deps.UUIDs]] deps = ["Random", "SHA"] diff --git a/docs/make.jl b/docs/make.jl index 1c563049..2b3216ae 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -1,11 +1,12 @@ using SoleLogics +using SoleLogics.ManyValuedLogics using Documenter DocMeta.setdocmeta!(SoleLogics, :DocTestSetup, :(using SoleLogics); recursive = true) makedocs(; - modules = [SoleLogics], - authors = "Mauro Milella, Giovanni Pagliarini, Eduard I. Stan", + modules = [SoleLogics, SoleLogics.ManyValuedLogics], + authors = "Mauro Milella, Giovanni Pagliarini, Alberto Paparella, Eduard I. Stan", repo=Documenter.Remotes.GitHub("aclai-lab", "SoleLogics.jl"), sitename = "SoleLogics.jl", format = Documenter.HTML(; @@ -19,7 +20,7 @@ makedocs(; "Getting started" => "getting-started.md", "Introduction to Logics and Propositional Logic" => "base-logic.md", "Modal Logic" => "modal-logic.md", - "Fuzzy" => "fuzzy.md", + "Many-valued logics" => "many-valued-logics.md", "More on Formulas" => "more-on-formulas.md", "Hands On" => "hands-on.md" ], diff --git a/docs/src/many-valued-logics.md b/docs/src/many-valued-logics.md new file mode 100644 index 00000000..094a808f --- /dev/null +++ b/docs/src/many-valued-logics.md @@ -0,0 +1,76 @@ +```@meta +CurrentModule = SoleLogics.ManyValuedLogics +``` + +```@contents +Pages = ["many-valued-logics.md"] +``` + +# [Introduction](@id many-valued-logics-introduction) +SoleLogics also provides tools to work with [many-valued logics](https://en.wikipedia.org/wiki/Many-valued_logic) (e.g., fuzzy logics), that is, logics with more truth values other than the classical Boolean ones `⊤` and `⊥`. With many-valued logics, the truth values are elements of a bounded lattice, providing a partial order between them, which encodes a *truer than* relation. + +Most of the tools for dealing with these logics can be accessed by importing the ManyValuedLogics submodule: +```julia +using SoleLogics.ManyValuedLogics +``` + +# [Operation](@id many-valued-logics-operation) +```@docs +Operation +BinaryOperation +``` + +# [Axiom](@id many-valued-logics-axiom) +```@docs +Axiom +checkaxiom +``` + +## [Common axioms](@id many-valued-logics-common-axioms) +```@docs +Commutativity +Associativity +AbsorptionLaw +LeftIdentity +RightIdentity +IdentityElement +RightResidual +LeftResidual +ResiduationProperty +Implication1 +Implication2 +Implication3 +DistributiveLaw +``` + +# [Finite algebra](@id many-valued-logics-finite-algebra) +```@docs +FiniteAlgebra +``` + +## [Monoid](@id many-valued-logics-monoid) +```@docs +Monoid +CommutativeMonoid +``` + +## [Finite lattice](@id many-valued-logics-finite-lattice) +```@docs +FiniteLattice +FiniteBoundedLattice +FiniteResiduatedLattice +``` + +## [Finite algebra varieties](@id many-valued-logics-finite-algebra-varieties) +```@docs +FiniteFLewAlgebra +FiniteHeytingAlgebra +``` + +# [Order utilities](@id many-valued-logics-order-utilities) +```@docs +precedeq +precedes +succeedeq +succeedes +``` diff --git a/docs/src/fuzzy.md b/docs/src/old-code/many-valued-logics/heyting-algebras.md similarity index 100% rename from docs/src/fuzzy.md rename to docs/src/old-code/many-valued-logics/heyting-algebras.md diff --git a/src/SoleLogics.jl b/src/SoleLogics.jl index 5765222f..5639deb1 100644 --- a/src/SoleLogics.jl +++ b/src/SoleLogics.jl @@ -91,10 +91,21 @@ export AbstractWorlds, Worlds export Interval, Interval2D, OneWorld + +export AbstractRelation + +export GlobalRel, IdentityRel +export globalrel, identityrel + + include("modal-logic.jl") ############################################################################################ +include("many-valued-logics/ManyValuedLogics.jl") + +############################################################################################ + export LeftmostLinearForm, LeftmostConjunctiveForm, LeftmostDisjunctiveForm, Literal export subformulas, normalize @@ -105,14 +116,6 @@ include("syntax-utils.jl") ############################################################################################ -export HeytingTruth, HeytingAlgebra -export precedes, succeedes, precedeq, succeedeq # TODO move above. -export @heytingtruths, @heytingalgebra - -include("fuzzy.jl") - -############################################################################################ - include("interpretation-sets.jl") ############################################################################################ diff --git a/src/algebras/frames/full-dimensional-frame/Full1DFrame+IA.jl b/src/algebras/frames/full-dimensional-frame/Full1DFrame+IA.jl index 3e24fa50..791ed5cb 100644 --- a/src/algebras/frames/full-dimensional-frame/Full1DFrame+IA.jl +++ b/src/algebras/frames/full-dimensional-frame/Full1DFrame+IA.jl @@ -2,26 +2,26 @@ # Refer to [`IntervalRelation`](@ref). # Allen relations -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_A) = zip(Iterators.repeated(w.y), w.y+1:X(fr)+1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_Ai) = zip(1:w.x-1, Iterators.repeated(w.x)) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_L) = _intervals_in(w.y+1, X(fr)+1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_Li) = _intervals_in(1, w.x-1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_B) = zip(Iterators.repeated(w.x), w.x+1:w.y-1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_Bi) = zip(Iterators.repeated(w.x), w.y+1:X(fr)+1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_E) = zip(w.x+1:w.y-1, Iterators.repeated(w.y)) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_Ei) = zip(1:w.x-1, Iterators.repeated(w.y)) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_D) = _intervals_in(w.x+1, w.y-1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_Di) = Iterators.product(1:w.x-1, w.y+1:X(fr)+1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_O) = Iterators.product(w.x+1:w.y-1, w.y+1:X(fr)+1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_Oi) = Iterators.product(1:w.x-1, w.x+1:w.y-1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_A) = zip(Iterators.repeated(w.y), w.y+1:X(fr)+1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_Ai) = zip(1:w.x-1, Iterators.repeated(w.x)) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_L) = _intervals_in(w.y+1, X(fr)+1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_Li) = _intervals_in(1, w.x-1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_B) = zip(Iterators.repeated(w.x), w.x+1:w.y-1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_Bi) = zip(Iterators.repeated(w.x), w.y+1:X(fr)+1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_E) = zip(w.x+1:w.y-1, Iterators.repeated(w.y)) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_Ei) = zip(1:w.x-1, Iterators.repeated(w.y)) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_D) = _intervals_in(w.x+1, w.y-1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_Di) = Iterators.product(1:w.x-1, w.y+1:X(fr)+1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_O) = Iterators.product(w.x+1:w.y-1, w.y+1:X(fr)+1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_Oi) = Iterators.product(1:w.x-1, w.x+1:w.y-1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_AorO) = Iterators.product(w.x+1:w.y, w.y+1:X(fr)+1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_AiorOi) = Iterators.product(1:w.x-1, w.x:w.y-1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_AorO) = Iterators.product(w.x+1:w.y, w.y+1:X(fr)+1) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_AiorOi) = Iterators.product(1:w.x-1, w.x:w.y-1) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_DorBorE) = Iterators.flatten((_accessibles(fr, w, IA_B), _accessibles(fr, w, IA_D), _accessibles(fr, w, IA_E))) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_DiorBiorEi) = Iterators.flatten((_accessibles(fr, w, IA_Bi), _accessibles(fr, w, IA_Di), _accessibles(fr, w, IA_Ei))) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_DorBorE) = Iterators.flatten((_accessibles(fr, w, IA_B), _accessibles(fr, w, IA_D), _accessibles(fr, w, IA_E))) +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_DiorBiorEi) = Iterators.flatten((_accessibles(fr, w, IA_Bi), _accessibles(fr, w, IA_Di), _accessibles(fr, w, IA_Ei))) -_accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_I) = Iterators.flatten(( +_accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_I) = Iterators.flatten(( # Iterators.product(1:w.x-1, w.y+1:X(fr)+1), # Di # Iterators.product(w.x:w.y, w.y+1:X(fr)+1), # A+O+Bi Iterators.product(1:w.y, w.y+1:X(fr)+1), # Di+A+O+Bi diff --git a/src/algebras/frames/full-dimensional-frame/Full2DFrame+IA2D.jl b/src/algebras/frames/full-dimensional-frame/Full2DFrame+IA2D.jl index c7118dc0..628e6a8a 100644 --- a/src/algebras/frames/full-dimensional-frame/Full2DFrame+IA2D.jl +++ b/src/algebras/frames/full-dimensional-frame/Full2DFrame+IA2D.jl @@ -4,7 +4,7 @@ # Convenience function _accessibles__(fr::Full1DFrame, w::Interval, r::IntervalRelation) = _accessibles(fr, w, r) _accessibles__(fr::Full1DFrame, w::Interval, r::IdentityRel, args...) = [(w.x, w.y)] -_accessibles__(fr::Full1DFrame, w::Interval{Int}, r::GlobalRel) = _intervals_in(1, X(fr)+1) +_accessibles__(fr::Full1DFrame, w::Interval{<:Integer}, r::GlobalRel) = _intervals_in(1, X(fr)+1) # Accessibles are easily coded using methods for one-dimensional interval logic _accessibles(fr::Full2DFrame, w::Interval2D, r::RectangleRelation) = diff --git a/src/algebras/frames/full-dimensional-frame/FullDimensionalFrame-filtered.jl b/src/algebras/frames/full-dimensional-frame/FullDimensionalFrame-filtered.jl new file mode 100644 index 00000000..1e2320e7 --- /dev/null +++ b/src/algebras/frames/full-dimensional-frame/FullDimensionalFrame-filtered.jl @@ -0,0 +1,366 @@ +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_A,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return zip(Iterators.repeated(w.y), w.y+1:min(w.y+worldfilter(r).k,X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_A, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return zip(Iterators.repeated(w.y), w.y+worldfilter(r).k:X(fr)+1) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_A,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return w.y+worldfilter(r).k < X(fr)+2 ? [(w.y, w.y+worldfilter(r).k)] : W[] +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Ai,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return zip(max(w.x-worldfilter(r).k,1):w.x-1, Iterators.repeated(w.x)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Ai, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return zip(1:w.x-worldfilter(r).k, Iterators.repeated(w.x)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Ai,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return w.x-worldfilter(r).k > 0 ? [(w.x-worldfilter(r).k, w.x)] : W[] +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_L,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->xxxxxx w.y && w.x+worldfilter(r).k < X(fr)+2 ? [(w.x, w.x+worldfilter(r).k)] : W[] +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_E,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return zip(max(w.y-worldfilter(r).k,w.x+1):w.y-1, Iterators.repeated(w.y)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_E, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return zip(w.x+1:w.y-worldfilter(r).k, Iterators.repeated(w.y)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_E,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return w.y-worldfilter(r).k > w.x ? [(w.y-worldfilter(r).k, w.y)] : W[] +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Ei,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return zip(max(w.y-worldfilter(r).k,1):w.x-1, Iterators.repeated(w.y)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Ei, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return zip(1:min(w.y-worldfilter(r).k, w.x-1), Iterators.repeated(w.y)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Ei,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return w.y-worldfilter(r).k < w.x && w.y-worldfilter(r).k > 0 ? [(w.y-worldfilter(r).k, w.y)] : W[] +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_D,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->xxxy-x≤worldfilter(r).k, Iterators.product(1:w.x-1, w.y+1:X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Di, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->y-x≥worldfilter(r).k, Iterators.product(1:w.x-1, w.y+1:X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Di,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->y-x==worldfilter(r).k, Iterators.product(1:w.x-1, w.y+1:X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_O,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->y-x≤worldfilter(r).k, Iterators.product(w.x+1:w.y-1, w.y+1:X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_O, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->y-x≥worldfilter(r).k, Iterators.product(w.x+1:w.y-1, w.y+1:X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_O,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->y-x==worldfilter(r).k, Iterators.product(w.x+1:w.y-1, w.y+1:X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Oi,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->y-x≤worldfilter(r).k, Iterators.product(1:w.x-1, w.x+1:w.y-1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Oi, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->y-x≥worldfilter(r).k, Iterators.product(1:w.x-1, w.x+1:w.y-1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_Oi,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->y-x==worldfilter(r).k, Iterators.product(1:w.x-1, w.x+1:w.y-1)) +end + +# ################################################################################ +# ################################################################################ +# ################################################################################ + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AorO,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{Int}} + return Iterators.filter(((x,y),)->y-x≤r.wf.k, Iterators.product(w.x+1:w.y, w.y+1:X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AorO, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{Int}} + return Iterators.filter(((x,y),)->y-x≥r.wf.k, Iterators.product(w.x+1:w.y, w.y+1:X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AorO,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{Int}} + return Iterators.filter(((x,y),)->y-x==r.wf.k, Iterators.product(w.x+1:w.y, w.y+1:X(fr)+1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AiorOi,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{Int}} + return Iterators.filter(((x,y),)->y-x≤r.wf.k, Iterators.product(1:w.x-1, w.x:w.y-1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AiorOi, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{Int}} + return Iterators.filter(((x,y),)->y-x≥r.wf.k, Iterators.product(1:w.x-1, w.x:w.y-1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AiorOi,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{Int}} + return Iterators.filter(((x,y),)->y-x==r.wf.k, Iterators.product(1:w.x-1, w.x:w.y-1)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_DorBorE,IntervalLengthFilter{F,T,W}}) where {F<:Function,T<:Real,W<:Interval{Int}} + return Iterators.flatten(( + _accessibles(fr, w, FilteredRelation(IA_B,IntervalLengthFilter(r.wf.f,r.wf.k))), + _accessibles(fr, w, FilteredRelation(IA_D,IntervalLengthFilter(r.wf.f,r.wf.k))), + _accessibles(fr, w, FilteredRelation(IA_E,IntervalLengthFilter(r.wf.f,r.wf.k))) + )) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_DiorBiorEi,IntervalLengthFilter{F,T,W}}) where {F<:Function,T<:Real,W<:Interval{Int}} + return Iterators.flatten(( + _accessibles(fr, w, FilteredRelation(IA_Bi,IntervalLengthFilter(r.wf.f,r.wf.k))), + _accessibles(fr, w, FilteredRelation(IA_Di,IntervalLengthFilter(r.wf.f,r.wf.k))), + _accessibles(fr, w, FilteredRelation(IA_Ei,IntervalLengthFilter(r.wf.f,r.wf.k))) + )) +end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_DorBorE,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{Int}} +# return Iterators.flatten(( +# _accessibles(fr, w, FilteredRelation(IA_B,IntervalLengthFilter(≤,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_D,IntervalLengthFilter(≤,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_E,IntervalLengthFilter(≤,r.wf.k))) +# )) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_DorBorE, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{Int}} +# return Iterators.flatten(( +# _accessibles(fr, w, FilteredRelation(IA_B,IntervalLengthFilter(≥,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_D,IntervalLengthFilter(≥,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_E,IntervalLengthFilter(≥,r.wf.k))) +# )) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_DorBorE,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{Int}} +# return Iterators.flatten(( +# _accessibles(fr, w, FilteredRelation(IA_B,IntervalLengthFilter(==,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_D,IntervalLengthFilter(==,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_E,IntervalLengthFilter(==,r.wf.k))) +# )) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_DiorBiorEi,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{Int}} +# return Iterators.flatten(( +# _accessibles(fr, w, FilteredRelation(IA_Bi,IntervalLengthFilter(≤,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_Di,IntervalLengthFilter(≤,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_Ei,IntervalLengthFilter(≤,r.wf.k))) +# )) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_DiorBiorEi, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{Int}} +# return Iterators.flatten(( +# _accessibles(fr, w, FilteredRelation(IA_Bi,IntervalLengthFilter(≥,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_Di,IntervalLengthFilter(≥,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_Ei,IntervalLengthFilter(≥,r.wf.k))) +# )) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_DiorBiorEi,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{Int}} +# return Iterators.flatten(( +# _accessibles(fr, w, FilteredRelation(IA_Bi,IntervalLengthFilter(==,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_Di,IntervalLengthFilter(==,r.wf.k))), +# _accessibles(fr, w, FilteredRelation(IA_Ei,IntervalLengthFilter(==,r.wf.k))) +# )) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_I,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{Int}} +# Iterators.flatten(( +# Iterators.filter(((x,y),)->y-x≤r.wf.k, Iterators.product(1:w.y, w.y+1:X(fr)+1)), # Di+A+O+Bi +# Iterators.filter(((x,y),)->y-x≤r.wf.k, Iterators.product(1:w.x-1, w.x:w.y)), # Ai+Oi+Ei +# _accessibles(fr, w, FilteredRelation(IA_B,IntervalLengthFilter(≤,r.wf.k))), # B +# _accessibles(fr, w, FilteredRelation(IA_E,IntervalLengthFilter(≤,r.wf.k))), # E +# _accessibles(fr, w, FilteredRelation(IA_D,IntervalLengthFilter(≤,r.wf.k))) # D +# )) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_I,IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{Int}} +# Iterators.flatten(( +# Iterators.filter(((x,y),)->y-x≥r.wf.k, Iterators.product(1:w.y, w.y+1:X(fr)+1)), # Di+A+O+Bi +# Iterators.filter(((x,y),)->y-x≥r.wf.k, Iterators.product(1:w.x-1, w.x:w.y)), # Ai+Oi+Ei +# _accessibles(fr, w, FilteredRelation(IA_B,IntervalLengthFilter(≥,r.wf.k))), # B +# _accessibles(fr, w, FilteredRelation(IA_E,IntervalLengthFilter(≥,r.wf.k))), # E +# _accessibles(fr, w, FilteredRelation(IA_D,IntervalLengthFilter(≥,r.wf.k))) # D +# )) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_I,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{Int}} +# Iterators.flatten(( +# Iterators.filter(((x,y),)->y-x==r.wf.k, Iterators.product(1:w.y, w.y+1:X(fr)+1)), # Di+A+O+Bi +# Iterators.filter(((x,y),)->y-x==r.wf.k, Iterators.product(1:w.x-1, w.x:w.y)), # Ai+Oi+Ei +# _accessibles(fr, w, FilteredRelation(IA_B,IntervalLengthFilter(==,r.wf.k))), # B +# _accessibles(fr, w, FilteredRelation(IA_E,IntervalLengthFilter(==,r.wf.k))), # E +# _accessibles(fr, w, FilteredRelation(IA_D,IntervalLengthFilter(==,r.wf.k))) # D +# )) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{GlobalRel,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{Int}} +# return Iterators.filter(((x,y),)->((x((x((xy-x≤worldfilter(r).k, Iterators.product(w.x+1:w.y, w.y+1:X(fr)+1)) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AorO, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{<:Integer}} +# return Iterators.filter(((x,y),)->y-x≥worldfilter(r).k, Iterators.product(w.x+1:w.y, w.y+1:X(fr)+1)) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AorO,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} +# return Iterators.filter(((x,y),)->y-x==worldfilter(r).k, Iterators.product(w.x+1:w.y, w.y+1:X(fr)+1)) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AiorOi,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} +# return Iterators.filter(((x,y),)->y-x≤worldfilter(r).k, Iterators.product(1:w.x-1, w.x:w.y-1)) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AiorOi, IntervalLengthFilter{typeof(≥),T,W}}) where {T<:Real,W<:Interval{<:Integer}} +# return Iterators.filter(((x,y),)->y-x≥worldfilter(r).k, Iterators.product(1:w.x-1, w.x:w.y-1)) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_AiorOi,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} +# return Iterators.filter(((x,y),)->y-x==worldfilter(r).k, Iterators.product(1:w.x-1, w.x:w.y-1)) +# end + +# function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{_IA_DorBorE,IntervalLengthFilter{typeof(==),T,W}}) where {T<:Real,W<:Interval{<:Integer}} +# return Iterators.flatten(( +# _accessibles(fr, w, FilteredRelation(IA_B,worldfilter(r))), +# _accessibles(fr, w, FilteredRelation(IA_D,worldfilter(r))), +# _accessibles(fr, w, FilteredRelation(IA_E,worldfilter(r))) +# )) +# # return Iterators.filter(((x,y),)->xwf.f(y-x, wf.k), Iterators.product(1:w.y, w.y+1:X(fr)+1)), # Di+A+O+Bi + Iterators.filter(((x,y),)->wf.f(y-x, wf.k), Iterators.product(1:w.x-1, w.x:w.y)), # Ai+Oi+Ei + _accessibles(fr, w, FilteredRelation(IA_B,wf)), # B + _accessibles(fr, w, FilteredRelation(IA_E,wf)), # E + _accessibles(fr, w, FilteredRelation(IA_D,wf)) # D + )) +end diff --git a/src/algebras/frames/full-dimensional-frame/dimensional-world-filters.jl b/src/algebras/frames/full-dimensional-frame/dimensional-world-filters.jl new file mode 100644 index 00000000..d49644a4 --- /dev/null +++ b/src/algebras/frames/full-dimensional-frame/dimensional-world-filters.jl @@ -0,0 +1,44 @@ +struct IntervalLengthFilter{F<:Function,T<:Real,W<:Interval} <: WorldFilter{W} + f::F + k::T + + function IntervalLengthFilter{F,T,W}(f::F, k::T) where {F<:Function,T<:Real,W<:Interval} + return new{F,T,W}(f, k) + end + function IntervalLengthFilter{F,T}(f::F, k::T) where {F<:Function,T<:Real} + return IntervalLengthFilter{F,T,Interval{Int}}(f, k) # Default + end + function IntervalLengthFilter(f::F, k::T) where {F<:Function,T<:Real} + return IntervalLengthFilter{F,T}(f, k) + end + +end + +function filterworlds(wf::IntervalLengthFilter, worlds) # ::AbstractArray{W}) where {W<:Interval} + return Iterators.filter(w -> wf.f(Base.length(w), wf.k), worlds) +end + +function accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{<:AbstractRelation,IntervalLengthFilter{F,T,W}}) where {F<:Function,T<:Real,W<:Interval{<:Integer}} + return IterTools.imap(W, _accessibles(fr, w, r)) +end + +function accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{GlobalRel, IntervalLengthFilter{F, T, W}}) where {F<:Function, T<:Real, W<:Interval{<:Integer}} + return IterTools.imap(W, _accessibles(fr, w, r)) +end + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{<:AbstractRelation,IntervalLengthFilter{F,T,W}}) where {F<:Function,T<:Real,W<:Interval{<:Integer}} + return error("Please provide a method for _accessibles(fr::$(typeof(fr)), w::$(typeof(w)), r::$(typeof(r))).") +end + + +function _accessibles(fr::Full1DFrame, w::W, r::FilteredRelation{GlobalRel,IntervalLengthFilter{typeof(≤),T,W}}) where {T<:Real,W<:Interval{<:Integer}} + return Iterators.filter(((x,y),)->((x((x((x syntaxstring(SoleLogics.identityrel) -"=" - -julia> SoleLogics.converse(identityrel) -IdentityRel() -``` - -See also -[`globalrel`](@ref), -[`AbstractRelation`](@ref), -[`AbstractWorld`](@ref), -[`AbstractFrame`](@ref). -[`AbstractKripkeStructure`](@ref), -""" - -"""$(doc_identityrel)""" -struct IdentityRel <: AbstractRelation end; -"""$(doc_identityrel)""" -const identityrel = IdentityRel(); - -arity(::IdentityRel) = 2 - -syntaxstring(::IdentityRel; kwargs...) = "=" - -hasconverse(::IdentityRel) = true -converse(::IdentityRel) = identityrel -istoone(::IdentityRel) = true -issymmetric(::IdentityRel) = true -isreflexive(::IdentityRel) = true -istransitive(::IdentityRel) = true - -############################################################################################ - -doc_globalrel = """ - struct GlobalRel <: AbstractRelation end; - const globalrel = GlobalRel(); - -Singleton type for the global relation. This is a binary relation via which a world -accesses every other world within the frame. -The relation is also symmetric, reflexive and transitive. - -# Examples -```julia-repl -julia> syntaxstring(SoleLogics.globalrel) -"G" - -julia> SoleLogics.converse(globalrel) -GlobalRel() -``` - -See also -[`identityrel`](@ref), -[`AbstractRelation`](@ref), -[`AbstractWorld`](@ref), -[`AbstractFrame`](@ref). -[`AbstractKripkeStructure`](@ref), -""" - -"""$(doc_globalrel)""" -struct GlobalRel <: AbstractRelation end; -"""$(doc_globalrel)""" -const globalrel = GlobalRel(); - -arity(::GlobalRel) = 2 - -syntaxstring(::GlobalRel; kwargs...) = "G" - -hasconverse(::GlobalRel) = true -converse(::GlobalRel) = globalrel -issymmetric(::GlobalRel) = true -isreflexive(::GlobalRel) = true -istransitive(::GlobalRel) = true -isgrounding(::GlobalRel) = true - -############################################################################################ - -""" -A binary relation via which a world *is accessed* by every other world within the frame. -That is, the binary relation that leads to a world. - -See also -[`identityrel`](@ref), -[`AbstractRelation`](@ref), -[`AbstractWorld`](@ref), -[`AbstractFrame`](@ref). -[`AbstractKripkeStructure`](@ref), -""" -struct AtWorldRelation{W<:AbstractWorld} <: AbstractRelation - w::W -end; - -arity(::AtWorldRelation) = 2 - -syntaxstring(r::AtWorldRelation; kwargs...) = "@($(syntaxstring(r.w)))" - -hasconverse(::AtWorldRelation) = false -issymmetric(::AtWorldRelation) = false -isreflexive(::AtWorldRelation) = false -istransitive(::AtWorldRelation) = true -isgrounding(::AtWorldRelation) = true - -############################################################################################ - """ struct NamedRelation{T} <: AbstractRelation name::T @@ -170,9 +51,9 @@ name(r::NamedRelation) = r.name ############################################################################################ -include("relations/geometrical-relations.jl"); +include("relations/filtered-relations.jl"); ############################################################################################ -include("relations/filtered-relations.jl"); +include("relations/geometrical-relations.jl"); diff --git a/src/algebras/relations/IntervalAlgebra.jl b/src/algebras/relations/IntervalAlgebra.jl index 527259be..26a4807a 100644 --- a/src/algebras/relations/IntervalAlgebra.jl +++ b/src/algebras/relations/IntervalAlgebra.jl @@ -199,16 +199,19 @@ istransitive(r::_IA_DorBorE) = true istransitive(r::_IA_DiorBiorEi) = true istopological(r::_IA_I) = true -IA72IARelations(::_IA_AorO) = [IA_A, IA_O] -IA72IARelations(::_IA_AiorOi) = [IA_Ai, IA_Oi] -IA72IARelations(::_IA_DorBorE) = [IA_D, IA_B, IA_E] -IA72IARelations(::_IA_DiorBiorEi) = [IA_Di, IA_Bi, IA_Ei] -IA32IARelations(::_IA_I) = [ +const IA7Relation = Union{_IA_AorO,_IA_AiorOi,_IA_DorBorE,_IA_DiorBiorEi} +IA72IARelations(::_IA_AorO) = (IA_A, IA_O) +IA72IARelations(::_IA_AiorOi) = (IA_Ai, IA_Oi) +IA72IARelations(::_IA_DorBorE) = (IA_D, IA_B, IA_E) +IA72IARelations(::_IA_DiorBiorEi) = (IA_Di, IA_Bi, IA_Ei) +syntaxstring(r::IA7Relation; kwargs...) = join(map(_r->syntaxstring(_r; kwargs...), IA72IARelations(r)), "") + +const IA3Relation = Union{_IA_I} +IA32IARelations(::_IA_I) = ( IA_A, IA_O, IA_D, IA_B, IA_E, IA_Ai, IA_Oi, IA_Di, IA_Bi, IA_Ei -] +) -syntaxstring(r::Union{_IA_AorO,_IA_DorBorE,_IA_AiorOi,_IA_DiorBiorEi}; kwargs...) = join(map(_r->syntaxstring(_r; kwargs...), IA72IARelations(r)), "") syntaxstring(::_IA_I; kwargs...) = "I" ############################################################################################ @@ -239,7 +242,6 @@ See also """ const IA7Relations = [IA_AorO, IA_L, IA_DorBorE, IA_AiorOi, IA_Li, IA_DiorBiorEi] -IA7Relation = Union{typeof.(IA7Relations)...} """ const IA3Relations = [IA_I, IA_L, IA_Li] @@ -251,7 +253,6 @@ See also [`IntervalRelation`](@ref), [`GeometricalRelation`](@ref). """ const IA3Relations = [IA_I, IA_L, IA_Li] -IA3Relation = Union{typeof.(IA3Relations)...} """ const IARelations_extended = [globalrel, IARelations...] diff --git a/src/algebras/relations/filtered-relations.jl b/src/algebras/relations/filtered-relations.jl index b8c02507..6d6e98a1 100644 --- a/src/algebras/relations/filtered-relations.jl +++ b/src/algebras/relations/filtered-relations.jl @@ -1,70 +1,117 @@ +abstract type WorldFilter{W<:AbstractWorld} end + +function filterworlds(wf::WorldFilter, worlds) # ::AbstractArray{W}) where {W<:AbstractWorld} + return error("Please, provide method filterworlds(::$(typeof(wf)), ::$(typeof(worlds))).") +end + +function (wf::WorldFilter)(worlds) # ::AbstractArray{W}) where {W<:AbstractWorld} + return filterworlds(wf, worlds) +end + using FunctionWrappers using FunctionWrappers: FunctionWrapper -abstract type WorldFilter{W <: AbstractWorld} end """ - struct FunctionalWorldFilter{W <: AbstractWorld, F <: Function} <: WorldFilter{W} - filter::FunctionWrapper{Bool, Tuple{W}} - end + struct FunctionalWorldFilter{W <: AbstractWorld, F <: Function} <: WorldFilter{W} + filter::FunctionWrapper{Bool, Tuple{W}} + end - FunctionalWorldFilter{W, F}(filter::FunctionWrapper{Bool, Tuple{W}}) where {W <: AbstractWorld, F <: Function} - FunctionalWorldFilter(filter::FunctionWrapper{Bool, Tuple{W}}, functiontype::Type{F}) where {W <: AbstractWorld, F <: Function} - FunctionalWorldFilter{W, F}(filter::F) where {W <: AbstractWorld, F <: Function} - FunctionalWorldFilter{W}(filter::F) where {W <: AbstractWorld, F <: Function} - FunctionalWorldFilter(filter::F, worldtype::Type{W}) where {W <: AbstractWorld, F <: Function} + FunctionalWorldFilter{W, F}(filter::FunctionWrapper{Bool, Tuple{W}}) where {W <: AbstractWorld, F <: Function} + FunctionalWorldFilter(filter::FunctionWrapper{Bool, Tuple{W}}, functiontype::Type{F}) where {W <: AbstractWorld, F <: Function} + FunctionalWorldFilter{W, F}(filter::F) where {W <: AbstractWorld, F <: Function} + FunctionalWorldFilter{W}(filter::F) where {W <: AbstractWorld, F <: Function} + FunctionalWorldFilter(filter::F, worldtype::Type{W}) where {W <: AbstractWorld, F <: Function} Please provide a function as filter so that it takes as input an object subtype of AbstractWorld and it gives as output a Bool. """ -struct FunctionalWorldFilter{W <: AbstractWorld, F <: Function} <: WorldFilter{W} - filter::FunctionWrapper{Bool, Tuple{W}} +struct FunctionalWorldFilter{W<:AbstractWorld,F<:Function} <: WorldFilter{W} + filter::FunctionWrapper{Bool,Tuple{W}} - function FunctionalWorldFilter{W, F}(filter::FunctionWrapper{Bool, Tuple{W}}) where {W <: AbstractWorld, F <: Function} - return new{W, F}(filter) + function FunctionalWorldFilter{W,F}(filter::FunctionWrapper{Bool,Tuple{W}}) where {W<:AbstractWorld,F<:Function} + return new{W,F}(filter) end - function FunctionalWorldFilter{W}(filter::FunctionWrapper{Bool, Tuple{W}}, functiontype::Type{F}) where {W <: AbstractWorld, F <: Function} - return new{W, functiontype}(filter) + function FunctionalWorldFilter{W}(filter::FunctionWrapper{Bool,Tuple{W}}, functiontype::Type{F}) where {W<:AbstractWorld,F<:Function} + return new{W,functiontype}(filter) end - function FunctionalWorldFilter(filter::FunctionWrapper{Bool, Tuple{W}}, functiontype::Type{F}) where {W <: AbstractWorld, F <: Function} + function FunctionalWorldFilter(filter::FunctionWrapper{Bool,Tuple{W}}, functiontype::Type{F}) where {W<:AbstractWorld,F<:Function} return FunctionalWorldFilter{W}(filter, functiontype) end - function FunctionalWorldFilter(filter::FunctionWrapper{Bool, Tuple{W}}) where {W <: AbstractWorld} - @warn "FunctionalWorldFilter initialized without specifying the functiontype.\n"* - "Please consider using the following syntax instead:\n"* - " FunctionalWorldFilter(FunctionWrapper{Bool, Tuple{W}}(filter), typeof(filter))\n"* + function FunctionalWorldFilter(filter::FunctionWrapper{Bool,Tuple{W}}) where {W<:AbstractWorld} + @warn "FunctionalWorldFilter initialized without specifying the functiontype.\n" * + "Please consider using the following syntax instead:\n" * + " FunctionalWorldFilter(FunctionWrapper{Bool, Tuple{W}}(filter), typeof(filter))\n" * "where W is a subtype of AbstractWorld and filter is a Function." return FunctionalWorldFilter(filter, Function) end - function FunctionalWorldFilter{W, F}(filter::F) where {W <: AbstractWorld, F <: Function} - return FunctionalWorldFilter{W, F}(FunctionWrapper{Bool, Tuple{W}}(filter)) + function FunctionalWorldFilter{W,F}(filter::F) where {W<:AbstractWorld,F<:Function} + return FunctionalWorldFilter{W,F}(FunctionWrapper{Bool,Tuple{W}}(filter)) end - function FunctionalWorldFilter{W}(filter::F) where {W <: AbstractWorld, F <: Function} - return FunctionalWorldFilter{W, F}(filter) + function FunctionalWorldFilter{W}(filter::F) where {W<:AbstractWorld,F<:Function} + return FunctionalWorldFilter{W,F}(filter) end - function FunctionalWorldFilter(filter::F, worldtype::Type{W}) where {W <: AbstractWorld, F <: Function} + function FunctionalWorldFilter(filter::F, worldtype::Type{W}) where {W<:AbstractWorld,F<:Function} return FunctionalWorldFilter{worldtype}(filter) end - function FunctionalWorldFilter(filter::F) where {F <: Function} - @warn "FunctionalWorldFilter initialized without specifying the worldtype.\n"* - "Plese consider using the following syntax instead:\n"* - " FunctionalWorldFilter(filter, worldtype)\n"* + function FunctionalWorldFilter(filter::F) where {F<:Function} + @warn "FunctionalWorldFilter initialized without specifying the worldtype.\n" * + "Plese consider using the following syntax instead:\n" * + " FunctionalWorldFilter(filter, worldtype)\n" * "where worldtype is a subtype of AbstractWorld and filter is a Function." return FunctionalWorldFilter(filter, AbstractWorld) end end -# Helper -Base.filter(f::FunctionalWorldFilter, a::Array{T, N}) where {T, N} = filter(f.filter, a) +function filterworlds(wf::FunctionalWorldFilter, worlds) # ::AbstractArray{W}) where {W<:AbstractWorld} + return Iterators.filter(wf.filter, worlds) +end -struct FilteredRelation{R <: AbstractRelation, F <: WorldFilter} +""" + struct FilteredRelation{R<:AbstractRelation,F<:WorldFilter} <: AbstractRelation + r::R + wf::F + end + +A (binary) accessibility relation `r`, filtered by a world filter `wf`. +""" +struct FilteredRelation{R<:AbstractRelation,F<:WorldFilter} <: AbstractRelation r::R - f::F + wf::F + + function FilteredRelation{R,F}(r::R, wf::F) where {R<:AbstractRelation,F<:WorldFilter} + return new(r, wf) + end + + function FilteredRelation(r::R, wf::F) where {R<:AbstractRelation,F<:WorldFilter} + return FilteredRelation{R,F}(r, wf) + end + + # TODO constructor that accepts a Callable and wraps it into a FunctionalWorldFilter? +end + +wrappedrelation(r::FilteredRelation) = r.r +worldfilter(r::FilteredRelation) = r.wf + +function accessibles( + fr::AbstractMultiModalFrame, + w::W, + r::FilteredRelation +) where {W <: AbstractWorld} + return filterworlds(worldfilter(r), IterTools.imap(W, _accessibles(fr, w, r.r))) +end + +function accessibles( + fr::AbstractMultiModalFrame, + ::W, + r::FilteredRelation{GlobalRel,<:WorldFilter{W}} +) where {W <: AbstractWorld} + return filterworlds(worldfilter(r), accessibles(fr, r.r)) end diff --git a/src/algebras/worlds/geometrical-worlds.jl b/src/algebras/worlds/geometrical-worlds.jl index 1622f09e..841f895f 100644 --- a/src/algebras/worlds/geometrical-worlds.jl +++ b/src/algebras/worlds/geometrical-worlds.jl @@ -1,3 +1,5 @@ +import Base: length + """ abstract type GeometricalWorld <: AbstractWorld end @@ -47,7 +49,10 @@ struct Point{N,T} <: GeometricalWorld Point(xyz::Vararg) = Point(xyz) end -Base.show(io::IO, w::Point) = print(io, "❮$(join(w.xyz, ","))❯") +# Base.size(w::Point) = (1,) # TODO maybe not +Base.length(w::Point) = 1 + +inlinedisplay(w::Point) = "❮$(join(w.xyz, ","))❯" Base.getindex(w::Point, args...) = Base.getindex(w.xyz, args...) @@ -113,6 +118,9 @@ struct Interval{T} <: GeometricalWorld # Interval(x,y) = x>0 && y>0 && x < y ? new(x,y) : error("Cannot instantiate Interval(x={$x},y={$y})") end +# Base.size(w::Interval) = (Base.length(w),) +Base.length(w::Interval) = (w.y - w.x) + inlinedisplay(w::Interval) = "($(w.x)−$(w.y))" goeswithdim(::Type{<:Interval}, ::Val{1}) = true @@ -166,6 +174,9 @@ struct Interval2D{T} <: GeometricalWorld Interval2D(x::Tuple{T,T}, y::Tuple{T,T}) where {T} = Interval2D{T}(x,y) end +# Base.size(w::Interval2D) = (Base.length(w.x), Base.length(w.y)) +Base.length(w::Interval2D) = prod(Base.length(w.x), Base.length(w.y)) + inlinedisplay(w::Interval2D) = "($(w.x)×$(w.y))" goeswithdim(::Type{<:Interval2D}, ::Val{2}) = true diff --git a/src/core.jl b/src/core.jl index 93677ca5..1faea428 100644 --- a/src/core.jl +++ b/src/core.jl @@ -50,7 +50,8 @@ function syntaxstring(s::Syntactical; kwargs...)::String end function Base.show(io::IO, φ::Syntactical) - print(io, "$(typeof(φ))\nsyntaxstring: $(syntaxstring(φ))") + # print(io, "$(typeof(φ))\nsyntaxstring: $(syntaxstring(φ))") + print(io, "$(typeof(φ)) with syntaxstring: $(syntaxstring(φ))") end ############################################################################################ @@ -702,7 +703,7 @@ function (op::Operator)(φs::NTuple{N,Formula}) where {N} φs = (op(φs[1:end-1]), φs[end]) end end - AbstractSyntaxStructure + if AbstractSyntaxStructure <: typejoin(typeof.(φs)...) φs = Base.promote(φs...) end diff --git a/src/many-valued-logics/ManyValuedLogics.jl b/src/many-valued-logics/ManyValuedLogics.jl new file mode 100644 index 00000000..1e626f4a --- /dev/null +++ b/src/many-valued-logics/ManyValuedLogics.jl @@ -0,0 +1,22 @@ +module ManyValuedLogics + +using ..SoleLogics + +export BinaryOperation + +include("operations.jl") + +include("axioms.jl") + +export FiniteTruth +export Monoid, CommutativeMonoid +export FiniteLattice, FiniteBoundedLattice, FiniteResiduatedLattice +export FiniteFLewAlgebra, FiniteHeytingAlgebra + +include("finite-algebras.jl") + +export precedeq, precedes, succeedeq, succeedes + +include("order-utilities.jl") + +end diff --git a/src/many-valued-logics/axioms.jl b/src/many-valued-logics/axioms.jl new file mode 100644 index 00000000..80b7cf9b --- /dev/null +++ b/src/many-valued-logics/axioms.jl @@ -0,0 +1,296 @@ +############################################################################################ +#### Axiom ################################################################################# +############################################################################################ + +""" + struct Axiom{Symbol} end + +An axiom is a statement that is taken to be true, to serve as a premise or starting point +for further reasoning and arguments. Axioms aim to capture what is special about +a particular structure (or set of structures). + +See also [`checkaxiom`](@ref). +""" +struct Axiom{Symbol} end + +""" + function checkaxiom(a::Axiom, args...) + +Check if axiom `a` is satisfied. + +See also [`Axiom`](@ref). +""" +function checkaxiom(a::Axiom, args...) + error("Please, provide a checkaxiom method for axiom $a.") +end + +""" + function Base.show(io::IO, a::Axiom) + +Write a text representation of an axiom to the output stream `io`. + +See also [`Axiom`](@ref). +""" +function Base.show(io::IO, ::Axiom{S}) where {S} + print(io, string(S)) +end + +############################################################################################ +#### Common axioms ######################################################################### +############################################################################################ + +""" + const Commutativity + +A binary operation * on a set S is called commutative if x * y = y * x ∀ x, y ∈ S. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref), [`checkaxiom`](@ref). +""" +const Commutativity = Axiom{:COM}() + +""" + function checkaxiom( + ::typeof(Commutativity), + o::BinaryOperation{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +A binary operation * on a set S is called commutative if x * y = y * x ∀ x, y ∈ S. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref). +""" +function checkaxiom( + ::typeof(Commutativity), + o::BinaryOperation{T,D} +) where { + T<:Truth, + D<:AbstractSet{T} +} + for i ∈ getdomain(o) + for j ∈ getdomain(o) + o(i, j) != o(j, i) && return false + end + end + return true +end + +# Helper +function iscommutative(o::BinaryOperation{T,D}) where {T<:Truth, D<:AbstractSet{T}} + return checkaxiom(Commutativity, o) +end + +""" + const Associativity + +A binary operation * on a set S is called associative if it satisfies the associative law: +(x * y) * z = x * (y * z) ∀ x, y, z ∈ S. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref), [`checkaxiom`](@ref). +""" +const Associativity = Axiom{:ASS}() + +""" + function checkaxiom( + ::typeof(Associativity), + o::BinaryOperation{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +A binary operation * on a set S is called associative if it satisfies the associative law: +(x * y) * z = x * (y * z) ∀ x, y, z ∈ S. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref). +""" +function checkaxiom( + ::typeof(Associativity), + o::BinaryOperation{T,D} +) where { + T<:Truth, + D<:AbstractSet{T} +} + for i ∈ getdomain(o) + for j ∈ getdomain(o) + for k ∈ getdomain(o) + o(o(i, j), k) != o(i, o(j, k)) && return false + end + end + end + return true +end + +# Helper +function isassociative(o::BinaryOperation{T,D}) where {T<:Truth, D<:AbstractSet{T}} + checkaxiom(Associativity, o) +end + +""" + const AbsorptionLaw + +The absorption law or absorption identity is an identity linking a pair of binary +operations. Two binary operations, * and ⋅, are said to be connected by the absorption law +if a * (a ⋅ b) = a ⋅ (a * b) = a. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref), [`checkaxiom`](@ref). +""" +const AbsorptionLaw = Axiom{:AL}() + +""" + function checkaxiom( + ::typeof(AbsorptionLaw), + o1::BinaryOperation{T,D}, + o2::BinaryOperation{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +The absorption law or absorption identity is an identity linking a pair of binary +operations. Two binary operations, * and ⋅, are said to be connected by the absotprion law +if a * (a ⋅ b) = a ⋅ (a * b) = a. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref). +""" +function checkaxiom( + ::typeof(AbsorptionLaw), + o1::BinaryOperation{T,D}, + o2::BinaryOperation{T,D} +) where { + T<:Truth, + D<:AbstractSet{T} +} + for i ∈ getdomain(o1) + for j ∈ getdomain(o1) + o1(i, o2(i, j)) != i && return false + o2(i, o1(i, j)) != i && return false + end + end + return true +end + +""" + const LeftIdentity + +Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a +left identity if e * s = s ∀ s ∈ S. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref), [`checkaxiom`](@ref). +""" +const LeftIdentity = Axiom{:LI}() + +""" + function checkaxiom( + ::typeof(LeftIdentity), + o::BinaryOperation{T,D}, + e::T + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a +left identity if e * s = s ∀ s ∈ S. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref). +""" +function checkaxiom( + ::typeof(LeftIdentity), + o::BinaryOperation{T,D}, + e::T +) where { + T<:Truth, + D<:AbstractSet{T} +} + for i ∈ getdomain(o) + o(e, i) != i && return false + end + return true +end + +""" + const RightIdentity + +Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a +right identity if s * e = s ∀ s ∈ S. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref), [`checkaxiom`](@ref). +""" +const RightIdentity = Axiom{:RI}() + +""" + function checkaxiom( + ::typeof(RightIdentity), + o::BinaryOperation{T,D}, + e::T + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Let (S, *) be a set S equipped with a binary operation *. Then an element e of S is called a +right identity if s * e = s ∀ s ∈ S. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref). +""" +function checkaxiom( + ::typeof(RightIdentity), + o::BinaryOperation{T,D}, + e::T +) where { + T<:Truth, + D<:AbstractSet{T} +} + for i ∈ getdomain(o) + o(i, e) != i && return false + end + return true +end + +""" + const IdentityElement + +An identity element or neutral element of a binary operation is an element that leaves +unchanged every element when the operation is applied. I.e., let (S, *) be a set S equipped +with a binary operation *. Then an element e of S is called a two-sided identity, or simply +identity, if e is both a left identity and a right identity. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref), [`LeftIdentity`](@ref), +[`RightIdentity`](@ref), [`checkaxiom`](@ref). +""" +const IdentityElement = Axiom{:IE}() + +""" + function checkaxiom( + ::typeof(IdentityElement), + o::BinaryOperation{T,D}, + e::T + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +An identity element or neutral element of a binary operation is an element that leaves +unchanged every element when the operation is applied. I.e., let (S, *) be a set S equipped +with a binary operation *. Then an element e of S is called a two-sided identity, or simply +identity, if e is both a left identity and a right identity. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref), [`LeftIdentity`](@ref), +[`RightIdentity`](@ref). +""" +function checkaxiom( + ::typeof(IdentityElement), + o::BinaryOperation{T,D}, + e::T +) where { + T<:Truth, + D<:AbstractSet{T} +} + if checkaxiom(LeftIdentity, o, e) && checkaxiom(RightIdentity, o, e) + return true + else + return false + end +end diff --git a/src/many-valued-logics/finite-algebras.jl b/src/many-valued-logics/finite-algebras.jl new file mode 100644 index 00000000..d3a00b17 --- /dev/null +++ b/src/many-valued-logics/finite-algebras.jl @@ -0,0 +1,1054 @@ +using ..SoleLogics: AbstractAlgebra +import ..SoleLogics: istop, isbot +import Base: convert + +############################################################################################ +#### Finite truth ########################################################################## +############################################################################################ + +struct FiniteTruth <: Truth + label::String + + function FiniteTruth(label::String) + return new(label) + end +end + +istop(t::FiniteTruth) = t.label == "⊤" +isbot(t::FiniteTruth) = t.label == "⊥" + +syntaxstring(t::FiniteTruth; kwargs...) = t.label +Base.show(io::IO, t::FiniteTruth) = print(io, syntaxstring(t)) + +function Base.convert(::Type{FiniteTruth}, t::BooleanTruth) + return istop(t) ? FiniteTruth("⊤") : FiniteTruth("⊥") +end + +function Base.isequal(t1::FiniteTruth, t2::BooleanTruth) + return (istop(t1) && istop(t2)) || (isbot(t1) && isbot(t2)) +end + +############################################################################################ +#### Finite algebra ######################################################################## +############################################################################################ + +""" + abstract type FiniteAlgebra{T<:Truth, D<:AbstractSet{T}} <: AbstractAlgebra{T} end + +A finite algebra is an algebraic structure defined over a finite set. + +See also [`AbstractAlgebra`](@ref). +""" +abstract type FiniteAlgebra{T<:Truth, D<:AbstractSet{T}} <: AbstractAlgebra{T} end + +############################################################################################ +#### Monoid ################################################################################ +############################################################################################ + +""" + function checkmonoidaxioms( + o::BinaryOperation{T,D}, + e::T + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check if given domain, operation and identity element form a monoid. + +A monoid (S, ⋅, e) is a set S equipped with a binary operation S × S → S, denoted as ⋅, +satisfying the following axiomatic identities: + - (Associativity) ∀ a, b, c ∈ S, the equation (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c) holds. + - (Identity element) There exists an element e ∈ L such that for every element a ∈ S, the + equalities e ⋅ a = a and a ⋅ e = a hold. + +The identity element of a monoid is unique. + +See also [`BinaryOperation`](@ref), [`Axiom`](@ref), [`checkaxiom`](@ref), +[`Associativity`](@ref), [`IdentityElement`](@ref). +""" +function checkmonoidaxioms( + o::BinaryOperation{T,D}, + e::T +) where { + T<:Truth, + D<:AbstractSet{T} +} + @assert checkaxiom(Associativity, o) "Defined an operation for the monoid which " * + "is not associative." + @assert checkaxiom(IdentityElement, o, e) "$e is not a valid identity element for " * + "the defined operation." + return nothing +end + +""" + struct Monoid{T<:Truth, D<:AbstractSet{T}} + operation::BinaryOperation{T,D} + identityelement::T + end + +A monoid (S, ⋅, e) is a set S equipped with a binary operation S × S → S, denoted as ⋅, +satisfying the following axiomatic identities: + - (Associativity) ∀ a, b, c ∈ S, the equation (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c) holds. + - (Identity element) There exists an element e ∈ L such that for every element a ∈ S, the + equalities e ⋅ a = a and a ⋅ e = a hold. + +The identity element of a monoid is unique. + +See also [`BinaryOperation`](@ref), [`Axiom`](@ref), [`checkaxiom`](@ref), +[`checkmonoidaxioms`](@ref), [`Associativity`](@ref), [`IdentityElement`](@ref). +""" +struct Monoid{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + operation::BinaryOperation{T,D} + identityelement::T + + function Monoid( + operation::BinaryOperation{T,D}, + identityelement::T + ) where { + T<:Truth, + D<:AbstractSet{T} + } + checkmonoidaxioms(operation, identityelement) + return new{T,D}(operation, identityelement) + end +end + +""" +Return true if the object can be converted to an object of type `Monoid`. + +See also [`Monoid`](@ref). +""" +ismonoid(::Monoid{T,D}) where {T<:Truth, D<:AbstractSet{T}} = true + +""" + function convert( + ::Type{Monoid}, + m::M + ) where { + T<:Truth, + D<:AbstractSet{T}, + M<:FiniteAlgebra{T,D} + } + +Convert `m` to a value of type `Monoid`. + +See also [`Monoid`](@ref), [`ismonoid`](@ref). +""" +function Base.convert( + ::Type{Monoid{T,D}}, + m::M +) where { + T<:Truth, + D<:AbstractSet{T}, + M<:FiniteAlgebra{T,D} +} + if ismonoid(m) + return Monoid(m.operation, m.identityelement) + else + error("Cannot convert object of type $(typeof(m)) to a value of type Monoid{$T,$D).") + end +end + +""" + function checkaxiom(a::Axiom, m::Monoid{T,D}) where {T<:Truth, D<:AbstractSet{T}} + +Check if axiom `a` is satisfied by the operation of the monoid `m`. + +See also [`Axiom`](@ref), [`Monoid`](@ref). +""" +function checkaxiom(a::Axiom, m::Monoid{T,D}) where {T<:Truth, D<:AbstractSet{T}} + return checkaxiom(typeof(a), m.operation) +end + +""" + function (m::Monoid{T,D})(t1::T, t2::T) where {T<:Truth, D<:AbstractSet{T}} + +Helper allowing to use monoids with function notation. + +See also [`Monoid`](@ref), [`BinaryOperation`](@ref). +""" +(m::Monoid{T,D})(t1::T, t2::T) where {T<:Truth, D<:AbstractSet{T}} = m.operation(t1, t2) + +############################################################################################ +#### Commutative monoid #################################################################### +############################################################################################ + +""" + struct CommutativeMonoid{T<:Truth, D<:AbstractSet{T}} + operation::BinaryOperation{T,D} + identityelement::T + end + +A commutative monoid (S, ⋅, e) is a monoid whose operation is commutative. + +See also [`Monoid`](@ref), [`Commutativity`](@ref). +""" +struct CommutativeMonoid{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + operation::BinaryOperation{T,D} + identityelement::T + + function CommutativeMonoid( + operation::BinaryOperation{T,D}, + identityelement + ) where { + T<:Truth, + D<:AbstractSet{T} + } + if !isa(identityelement, T) identityelement = convert(T, identityelement)::T end + checkmonoidaxioms(operation, identityelement) + @assert checkaxiom(Commutativity, operation) "Defined an operation for the " * + "commutative monoid which is not commutative." + return new{T,D}(operation, identityelement) + end +end + +ismonoid(::CommutativeMonoid{T,D}) where {T<:Truth, D<:AbstractSet{T}} = true + +""" + function (m::CommutativeMonoid{T,D})(t1::T, t2::T) where {T<:Truth, D<:AbstractSet{T}} + +Helper allowing to use commutative monoids with function notation. + +See also [`Monoid`](@ref), [`BinaryOperation`](@ref). +""" +function (m::CommutativeMonoid{T,D})(t1::T, t2::T) where {T<:Truth, D<:AbstractSet{T}} + return m.operation(t1, t2) +end + +############################################################################################ +#### Finite lattice ######################################################################## +############################################################################################ + +""" + function checklatticeaxioms( + join::BinaryOperation{T,D}, + meet::BinaryOperation{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check if given domain, join and meet form a finite lattice. + +A lattice is an algebraic structure (L, ∨, ∧) consisting of a set L and two binary, +commutative and associative operations ∨ and ∧ on L satisfying the following axiomatic +identities for all elements a, b ∈ L (sometimes called absorption laws): +- a ∨ (a ∧ b) = a +- a ∧ (a ∨ b) = a + +See also [`FiniteLattice`](@ref), [`BinaryOperation`](@ref), [`Commutativity`](@ref), +[`Associativity`](@ref), [`AbsorptionLaw`](@ref), +""" +function checklatticeaxioms( + join::BinaryOperation{T,D}, + meet::BinaryOperation{T,D} +) where { + T<:Truth, + D<:AbstractSet{T} +} + @assert checkaxiom(Commutativity, join) "Defined a join operation which is not " * + "commutative." + @assert checkaxiom(Associativity, join) "Defined a join operation which is not " * + "associative." + @assert checkaxiom(Commutativity, meet) "Defined a meet operation which is not " * + "commutative." + @assert checkaxiom(Associativity, meet) "Defined a meet operation which is not " * + "associative." + @assert checkaxiom(AbsorptionLaw, join, meet) "Absorption law does not hold between " * + "join and meet." + return nothing +end + +""" + struct FiniteLattice{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + end + +A finite lattice is a lattice defined over a finite set. + +A lattice is an algebraic structure (L, ∨, ∧) consisting of a set L and two binary, +commutative and associative operations ∨ and ∧ on L satisfying the following axiomatic +identities for all elements a, b ∈ L (sometimes called absorption laws): + - a ∨ (a ∧ b) = a + - a ∧ (a ∨ b) = a + +See also [`FiniteAlgebra`](@ref), [`BinaryOperation`](@ref). +""" +struct FiniteLattice{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + + function FiniteLattice( + join::BinaryOperation{T,D}, + meet::BinaryOperation{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + checklatticeaxioms(join, meet) + return new{T,D}(join, meet) + end +end + +""" +Return true if the object can be converted to an object of type `FiniteLattice`. + +See also [`FiniteLattice`](@ref). +""" +islattice(::FiniteLattice{T,D}) where {T<:Truth, D<:AbstractSet{T}} = true + +""" + function convert( + ::Type{FiniteLattice}, + l::L + ) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} + } + +Convert `l` to a value of type `FiniteLattice`. + +See also [`FiniteLattice`](@ref), [`islattice`](@ref). +""" +function convert( + ::Type{FiniteLattice}, + l::L +) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} +} + if islattice(l) + return FiniteLattice(l.join, l.meet) + else + error("Cannot convert object of type $(typeof(l)) to a value of type Lattice.") + end +end + +""" + function getdomain(a::A) where {T<:Truth, D<:AbstractSet{T}, L<:FiniteAlgebra{T,D}} + +Return the domain associated to `a`. + +See also [`Monoid`](@ref), [`FiniteLattice`](@ref), [`ismonoid`](@ref), [`islattice`](@ref). +""" +function getdomain(a::A) where {T<:Truth, D<:AbstractSet{T}, A<:FiniteAlgebra{T,D}} + if ismonoid(a) + return getdomain(a.operation) + elseif islattice(a) + return getdomain(a.join) + else + error("Cannot convert object of type $(typeof(l)) to a value of type Monoid.") + end +end + +############################################################################################ +#### Finite bounded lattice ################################################################ +############################################################################################ + +""" + function checkboundedlatticeaxioms( + join::BinaryOperation{T,D}, + meet::BinaryOperation{T,D}, + bot::T, + top::T + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check if given domain, join, meet, bot and top form a bounded lattice. + +A bounded lattice is an algebraic structure (L, ∨, ∧, ⊥, ⊤) such that (L, ∨, ∧) is a +lattice, the bottom element ⊥ is the identity element for the join operation ∨, and the top +element ⊤ is the identity element for the meet operation ∧: + - a ∨ ⊥ = a + - a ∧ ⊤ = a + +See also [`FiniteBoundedLattice`](@ref), [`checklatticeaxioms`](@ref). +""" +function checkboundedlatticeaxioms( + join::BinaryOperation{T,D}, + meet::BinaryOperation{T,D}, + bot::T, + top::T +) where { + T<:Truth, + D<:AbstractSet{T} +} + checklatticeaxioms(join, meet) + @assert checkaxiom(IdentityElement, join, bot) "$bot is not a valid identity element " * + "for the defined join operation." + @assert checkaxiom(IdentityElement, meet, top) "$top is not a valid identity element " * + "for the defined meet operation." + return nothing +end + +""" + struct FiniteBoundedLattice{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + bot::T + top::T + end + +A finite bounded lattice is a bounded lattice defined over a finite set. + +A bounded lattice is an algebraic structure (L, ∨, ∧, ⊥, ⊤) such that (L, ∨, ∧) is a +lattice, the bottom element ⊥ is the identity element for the join operation ∨, and the top +element ⊤ is the identity element for the meet operation ∧: + - a ∨ ⊥ = a + - a ∧ ⊤ = a + +See also [`FiniteLattice`](@ref). +""" +struct FiniteBoundedLattice{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + bot::T + top::T + + function FiniteBoundedLattice( + join::BinaryOperation{T,D}, + meet::BinaryOperation{T,D}, + bot::T1, + top::T2 + ) where { + T<:Truth, + D<:AbstractSet{T}, + T1<:Truth, + T2<:Truth + } + if !isa(bot, T) bot = convert(T, bot)::T end + if !isa(top, T) top = convert(T, top)::T end + checkboundedlatticeaxioms(join, meet, bot, top) + return new{T,D}(join, meet, bot, top) + end +end + +islattice(::FiniteBoundedLattice{T,D}) where {T<:Truth, D<:AbstractSet{T}} = true + +""" +Return true if the object can be converted to an object of type `FiniteBoundedLattice`. + +See also [`FiniteBoundedLattice`](@ref). +""" +isboundedlattice(::FiniteBoundedLattice{T,D}) where {T<:Truth, D<:AbstractSet{T}} = true + +""" + function convert( + ::Type{FiniteBoundedLattice}, + l::L + ) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} + } + +Convert `l` to a value of type `FiniteBoundedLattice`. + +See also [`FiniteBoundedLattice`](@ref), [`isboundedlattice`](@ref). +""" +function convert( + ::Type{FiniteBoundedLattice}, + l::L +) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} +} + if isboundedlattice(l) + return FiniteBoundedLattice(l.join, l.meet, l.bot, l.top) + else + error("Cannot convert object of type $(typeof(l)) to a value of type Lattice.") + end +end + +############################################################################################ +#### Residuated lattice #################################################################### +############################################################################################ + +""" + const RightResidual + +The right residual between two elements z, x ∈ S is the greatest y ∈ S such that x ⋅ y ≤ z. + +See also [`Axiom`](@ref), [`Monoid`](@ref), [`checkaxiom`](@ref). +""" +const RightResidual = Axiom{:RR}() + +""" + function checkaxiom( + ::typeof(RightResidual), + m::Monoid{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check that ∀ x ∈ S there exists for every x ∈ S a greatest y ∈ S such that x ⋅ y ≤ z. + +See also [`Axiom`](@ref), [`Monoid`](@ref). +""" +function checkaxiom( + ::typeof(RightResidual), + meet::BinaryOperation{T,D}, + monoid::M +) where { + T<:Truth, + D<:AbstractSet{T}, + M<:FiniteAlgebra{T,D} +} + !ismonoid(monoid) && error("Cannot convert an object of type $(typeof(monoid)) to an "* + "object of type Monoid.") + for z ∈ getdomain(monoid) + for x ∈ getdomain(monoid) + candidates = Set{T}() + for y ∈ getdomain(monoid) + meet(monoid(x, y), z) == monoid(x, y) && push!(candidates, y) + end + foundrr = false + for y ∈ candidates + isgreatest = true + for w ∈ candidates + if meet(w, y) != w + isgreatest = false + break + end + end + if isgreatest + foundrr = true + break + end + end + !foundrr && return false + end + end + return true +end + +""" + const LeftResidual + +The left residual between two elements z, y ∈ S is the greatest x ∈ S such that x ⋅ y ≤ z. + +See also [`Axiom`](@ref), [`Monoid`](@ref), [`checkaxiom`](@ref). +""" +const LeftResidual = Axiom{:LR}() + +""" + function checkaxiom( + ::typeof(LeftResidual), + m::Monoid{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check that ∀ x ∈ S there exists for every y ∈ S a greatest x ∈ S such that x ⋅ y ≤ z. + +See also [`Axiom`](@ref), [`Monoid`](@ref). +""" +function checkaxiom( + ::typeof(LeftResidual), + meet::BinaryOperation{T,D}, + monoid::M +) where { + T<:Truth, + D<:AbstractSet{T}, + M<:FiniteAlgebra{T,D} +} + !ismonoid(monoid) && error("Cannot convert an object of type $(typeof(monoid)) to an "* + "object of type Monoid.") + for z ∈ getdomain(monoid) + for y ∈ getdomain(monoid) + candidates = Set{T}() + for x ∈ getdomain(monoid) + meet(monoid(x, y), z) == monoid(x, y) && push!(candidates, x) + end + foundlr = false + for x ∈ candidates + isgreatest = true + for w ∈ candidates + if meet(w, x) != w + isgreatest = false + break + end + end + if isgreatest + foundlr = true + break + end + end + !foundlr && return false + end + end + return true +end + +""" + const ResiduationProperty + +A lattice (L, ∨, ∧, ⋅, ⊥, →) is residuated if ∀ x ∈ S there exists for every x ∈ S a +greatest y ∈ S and for every y ∈ S a greatest x ∈ S such that x ⋅ y ≤ z. + +See also [`Axiom`](@ref), [`Monoid`](@ref), [`checkaxiom`](@ref). +""" +const ResiduationProperty = Axiom{:RP}() + +""" + function checkaxiom( + ::typeof(ResiduationProperty), + m::Monoid{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check that ∀ x ∈ S there exists for every x ∈ S a greatest y ∈ S and for every y ∈ S a +greatest x ∈ S such that x ⋅ y ≤ z. + +See also [`Axiom`](@ref), [`Monoid`](@ref). +""" +function checkaxiom( + ::typeof(ResiduationProperty), + meet::BinaryOperation{T,D}, + monoid::M +) where { + T<:Truth, + D<:AbstractSet{T}, + M<:FiniteAlgebra{T,D} +} + !ismonoid(monoid) && error("Cannot convert an object of type $(typeof(monoid)) to an "* + "object of type Monoid.") + if checkaxiom(RightResidual, meet, monoid) && checkaxiom(LeftResidual, meet, monoid) + return true + else + return false + end +end + +""" + struct FiniteResiduatedLattice{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + domain::D + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + monoid::Monoid{T,D} + rightresidual::BinaryOperation{T,D} + leftresidual::BinaryOperation{T,D} + bot::T + top::T + end + +A residuated lattice is an algebraic structure L = (L, ∨, ∧, ⋅, e) such that: + - (L, ∨, ∧) is a lattice + - (L, ⋅, e) is a monoid + - ∀ x ∈ L there exists for every x ∈ L a greatest y ∈ L and for every y ∈ L a greatest + x ∈ L such that x ⋅ y ≤ z + +See also [`FiniteBoundedLattice`](@ref), +""" +struct FiniteResiduatedLattice{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + monoid::Monoid{T,D} + rightresidual::BinaryOperation{T,D} + leftresidual::BinaryOperation{T,D} + bot::T + top::T + + function FiniteResiduatedLattice( + join::BinaryOperation{T,D}, + meet::BinaryOperation{T,D}, + monoid::M, + bot::T1, + top::T2 + ) where { + T<:Truth, + D<:AbstractSet{T}, + M<:FiniteAlgebra{T,D}, + T1<:Truth, + T2<:Truth + } + if !isa(monoid, Monoid{T,D}) monoid = convert(Monoid{T,D}, monoid)::Monoid{T,D} end + if !isa(bot, T) bot = convert(T, bot)::T end + if !isa(top, T) top = convert(T, top)::T end + checkboundedlatticeaxioms(join, meet, bot, top) + @assert checkaxiom(ResiduationProperty, meet, monoid) "Residuation property does " * + "not hold for the defined monoid operation." + rrtruthtable = Dict{Tuple{T, T}, T}() + lrtruthtable = Dict{Tuple{T, T}, T}() + for z ∈ getdomain(monoid) + for x ∈ getdomain(monoid) + candidates = Set{T}() + for y ∈ getdomain(monoid) + meet(monoid(x, y), z) == monoid(x, y) && push!(candidates, y) + end + for y ∈ candidates + isgreatest = true + for w ∈ candidates + if meet(w, y) != w + isgreatest = false + break + end + end + if isgreatest + rrtruthtable[(x,z)] = y + break + end + end + end + for y ∈ getdomain(monoid) + candidates = Set{T}() + for x ∈ getdomain(monoid) + meet(monoid(x, y), z) == monoid(x, y) && push!(candidates, y) + end + for x ∈ candidates + isgreatest = true + for w ∈ candidates + if meet(w, x) != w + isgreatest = false + break + end + end + if isgreatest + lrtruthtable[(y,z)] = x + break + end + end + end + end + rightresidual = BinaryOperation(getdomain(monoid), rrtruthtable) + leftresidual = BinaryOperation(getdomain(monoid), lrtruthtable) + return new{T,D}(join, meet, monoid, rightresidual, leftresidual, bot, top) + end +end + +############################################################################################ +#### Finite FLew algebra ################################################################### +############################################################################################ + +""" + struct FiniteFLewAlgebra{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + domain::D + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + monoid::Monoid{T,D} + implication::BinaryOperation{T,D} + bot::T + top::T + end + +An FLew-algebra is an algebra (L, ∨, ∧, ⋅, →, ⊥, ⊤), where +- (L, ∨, ∧, ⊥, ⊤) is a bounded lattice with top element ⊤ and bottom element ⊥ +- (L, ⋅, ⊤) is a commutative monoid +- The residuation property holds: x ⋅ y ≤ z iff x ≤ y → z + +See also [`FiniteBoundedLattice`](@ref), [`CommutativeMonoid`](@ref). +""" +struct FiniteFLewAlgebra{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + monoid::CommutativeMonoid{T,D} + implication::BinaryOperation{T,D} + bot::T + top::T + + function FiniteFLewAlgebra( + join::BinaryOperation{T,D}, + meet::BinaryOperation{T,D}, + monoid::CommutativeMonoid{T,D}, + bot::T1, + top::T2 + ) where { + T<:Truth, + D<:AbstractSet{T}, + T1<:Truth, + T2<:Truth + } + if !isa(bot, T) bot = convert(T, bot)::T end + if !isa(top, T) top = convert(T, top)::T end + checkboundedlatticeaxioms(join, meet, bot, top) + @assert checkaxiom(RightResidual, meet, monoid) "Residuation property does not " * + "hold for the defined monoid operation." + implicationtruthtable = Dict{Tuple{T, T}, T}() + for z ∈ getdomain(monoid) + for x ∈ getdomain(monoid) + candidates = Set{T}() + for y ∈ getdomain(monoid) + meet(monoid(x, y), z) == monoid(x, y) && push!(candidates, y) + end + for y ∈ candidates + isgreatest = true + for w ∈ candidates + if meet(w, y) != w + isgreatest = false + break + end + end + if isgreatest + implicationtruthtable[(x,z)] = y + break + end + end + end + end + implication = BinaryOperation(getdomain(monoid), implicationtruthtable) + return new{T,D}(join, meet, monoid, implication, bot, top) + end +end + +islattice(::FiniteFLewAlgebra{T,D}) where {T<:Truth, D<:AbstractSet{T}} = true +isboundedlattice(::FiniteFLewAlgebra{T,D}) where {T<:Truth, D<:AbstractSet{T}} = true + +############################################################################################ +#### Finite Heyting algebra ################################################################ +############################################################################################ + +""" + const Implication1 + +Axiom Implication1 is satisfied if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and +smallest elements ⊤ and ⊥, and a binary operation →, a → a = ⊤ holds. + +See also [`Axiom`](@ref), [`checkaxiom`](@ref). +""" +const Implication1 = Axiom{:I1}() + +""" + function checkaxiom( + ::typeof(Implication1), + o::BinaryOperation{T,D}, + top::Truth + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, +and a binary operation →, a → a = ⊤ holds. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref). +""" +function checkaxiom( + ::typeof(Implication1), + o::BinaryOperation{T,D}, + top::Truth +) where { + T<:Truth, + D<:AbstractSet{T} +} + for i ∈ getdomain(o) + o(i, i) != top && return false + end + return true +end + +""" + const Implication2 + +Axiom Implication2 is satisfied if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary +operations ∧ (`o1`) and → (`o2`), a ∧ (a → b) = a ∧ b holds. + +See also [`Axiom`](@ref), [`checkaxiom`](@ref). +""" +const Implication2 = Axiom{:I2}() + +""" + function checkaxiom( + ::typeof(Implication2), + o1::BinaryOperation{T,D}, + o2::BinaryOperation{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, +and two binary operations ∧ (`o1`) and → (`o2`), a ∧ (a → b) = a ∧ b holds. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref). +""" +function checkaxiom( + ::typeof(Implication2), + o1::BinaryOperation{T,D}, + o2::BinaryOperation{T,D} +) where { + T<:Truth, + D<:AbstractSet{T} +} + for i ∈ getdomain(o1) + for j ∈ getdomain(o1) + o1(i, o2(i, j)) != o1(i, j) && return false + end + end + return true +end + +""" + const Implication3 + +Axiom Implication3 is satisfied if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary +operations ∧ (`o1`) and → (`o2`), b ∧ (a → b) = b holds. + +See also [`Axiom`](@ref), [`checkaxiom`](@ref). +""" +const Implication3 = Axiom{:I3}() + +""" + function checkaxiom( + ::typeof(Implication3), + o1::BinaryOperation{T,D}, + o2::BinaryOperation{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, +and two binary operations ∧ (`o1`) and → (`o2`), b ∧ (a → b) = b holds. + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref). +""" +function checkaxiom( + ::typeof(Implication3), + o1::BinaryOperation{T,D}, + o2::BinaryOperation{T,D} +) where { + T<:Truth, + D<:AbstractSet{T} +} + for i ∈ getdomain(o1) + for j ∈ getdomain(o1) + o1(j, o2(i, j)) != j && return false + end + end + return true +end + +""" + const DistributiveLaw + +Given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary operations ⋅ and *, ⋅ is +distributive over * if ∀ a, b, c ∈ L: a ⋅ (b * c) = (a ⋅ b) * (a ⋅ c). + +See also [`Axiom`](@ref), [`checkaxiom`](@ref). +""" +const DistributiveLaw = Axiom{:DL}() + +""" + function checkaxiom( + ::typeof(DistributiveLaw), + o1::BinaryOperation{T,D}, + o2::BinaryOperation{T,D} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Check if given a bounded lattice (H, ∨, ∧, ⊥, ⊤) and two binary operations ⋅ and *, ⋅ is +distributive over * if ∀ a, b, c ∈ L: a ⋅ (b * c) = (a ⋅ b) * (a ⋅ c). + +See also [`Axiom`](@ref), [`BinaryOperation`](@ref). +""" +function checkaxiom( + ::typeof(DistributiveLaw), + o1::BinaryOperation{T,D}, + o2::BinaryOperation{T,D} +) where { + T<:Truth, + D<:AbstractSet{T} +} + for i ∈ getdomain(o1) + for j ∈ getdomain(o1) + for k ∈ getdomain(o1) + o1(i, o2(j, k)) != o2(o1(i, j), o1(i, k)) && return false + end + end + end + return true +end + +""" + struct FiniteHeytingAlgebra{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + domain::D + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + implication::BinaryOperation{T,D} + bot::T + top::T + end + +A Heyting algebra (H, ∨, ∧, →, ⊥, ⊤) is a bounded lattice (H, ∨, ∧, ⊥, ⊤) equipped with a +binary operation a → b of implication such that (c ∧ a) ≤ b is equivalent to c ≤ (a → b). + +Given a bounded lattice (H, ∨, ∧, ⊥, ⊤) with largest and smallest elements ⊤ and ⊥, and a +binary operation →, these together form a Heyting algebra if and only if the following hold: + - (Implication1) a → a = ⊤ + - (Implication2) a ∧ (a → b) = a ∧ b + - (Implication3) b ∧ (a → b) = b + - (Distributive law for →) a → (b ∧ c) = (a → b) ∧ (a → c) + +See also [`FiniteBoundedLattice`](@ref), [`BinaryOperation`](@ref). +""" +struct FiniteHeytingAlgebra{T<:Truth, D<:AbstractSet{T}} <: FiniteAlgebra{T,D} + join::BinaryOperation{T,D} + meet::BinaryOperation{T,D} + implication::BinaryOperation{T,D} + bot::T + top::T + + function FiniteHeytingAlgebra( + join::BinaryOperation{T,D}, + meet::BinaryOperation{T,D}, + implication::BinaryOperation{T,D},bot::T1, + top::T2 + ) where { + T<:Truth, + D<:AbstractSet{T}, + T1<:Truth, + T2<:Truth + } + if !isa(bot, T) bot = convert(T, bot)::T end + if !isa(top, T) top = convert(T, top)::T end + checkboundedlatticeaxioms(join, meet, bot, top) + @assert checkaxiom(Implication1, implication, top) "Axiom a → a = ⊤ does not " * + "hold for given binary operation →." + @assert checkaxiom(Implication2, meet, implication) "Axiom a ∧ (a → b) = a ∧ b " * + "does not hold for given binary operation →." + @assert checkaxiom(Implication3, meet, implication) "Axiom b ∧ (a → b) = b does " * + "not hold for given binary operation →." + @assert checkaxiom(DistributiveLaw, implication, meet) "Distributive law for → " * + "does not hold for given binary operation →." + return new{T,D}(join, meet, implication, bot, top) + end +end + +islattice(::FiniteHeytingAlgebra{T,D}) where {T<:Truth, D<:AbstractSet{T}} = true +isboundedlattice(::FiniteHeytingAlgebra{T,D}) where {T<:Truth, D<:AbstractSet{T}} = true + +""" + function convert( + ::Type{FiniteFLewAlgebra{T,D}}, + l::FiniteHeytingAlgebra + ) where { + T<:Truth, + D<:AbstractSet{T} + } + +Convert `l` of type `FiniteHeytingAlgebra` to a value of type `FiniteFLewAlgebra`. + +See also [`FiniteFLewAlgebra`](@ref), [`FiniteHeytingAlgebra`](@ref). +""" +function convert( + ::Type{FiniteFLewAlgebra{T,D}}, + l::FiniteHeytingAlgebra +) where { + T<:Truth, + D<:AbstractSet{T} +} + return FiniteFLewAlgebra(l.join, l.meet, l.meet, l.bot, l.top) +end diff --git a/src/many-valued-logics/operations.jl b/src/many-valued-logics/operations.jl new file mode 100644 index 00000000..c8c838b9 --- /dev/null +++ b/src/many-valued-logics/operations.jl @@ -0,0 +1,91 @@ +import SoleLogics: arity + +""" + abstract type Operation end + +An operation is a function which takes zero or more operands to a well-defined output value. + +See also [`BinaryOperation`](@ref), [`arity`](@ref). +""" +abstract type Operation end + +""" + function Base.show(io::IO, o::O) where {O<:Operation} + +Write a text representation of an operation `o` to the output stream `io`. + +See also [`Operation`](@ref), [`BinaryOperation`](@ref), [`arity`](@ref). +""" +function Base.show(io::IO, o::O) where {O<:Operation} + print(io, "$(typeof(o)) without a show function") + @warn "Please, provide a show function for operation $(typeof(o))." +end + +""" + function arity(o::O) where {O<:Operation} + +Return the arity of an operation `o`. + +See also [`Operation`](@ref), [`BinaryOperation`](@ref), [`arity`](@ref). +""" +function arity(o::O) where {O<:Operation} + error("Please, provide an arity for operation $o.") +end + +""" + struct BinaryOperation{T<:Truth, D<:AbstractSet{T}} <: Operation + domain::D + truthtable::AbstractDict{Tuple{T, T}, T} + end + +A binary operation on a set S is a mapping of the elements of the Cartesian product +S × S → S. The closure property of a binary operation expresses the existence of a result +for the operation given any pair of operands. Binary operations are required to be defined +on all elements of S × S. + +See also [`Operation`](@ref), [`arity`](@ref). +""" +struct BinaryOperation{T<:Truth, D<:AbstractSet{T}} <: Operation + domain::D + truthtable::AbstractDict{Tuple{T, T}, T} + + function BinaryOperation( + domain::D, + truthtable::Dict{Tuple{T, T}, T} + ) where { + T<:Truth, + D<:AbstractSet{T} + } + for i ∈ domain + for j ∈ domain + @assert (i, j) ∈ keys(truthtable) "truthtable[($i, $j)] is not defined." + end + end + @assert length(truthtable) == length(domain)^2 "Found truthtable[(i, j)] where i " * + "or j ∉ domain." + return new{T,D}(domain, truthtable) + end +end + +Base.show(io::IO, o::BinaryOperation) = print(io, "$(o.truthtable)") +arity(o::BinaryOperation) = 2 + +""" + function getdomain(o::BinaryOperation) + +Return the domain associated to binary operation `o`. + +See also [`BinaryOperation`](@ref). +""" +getdomain(o::BinaryOperation) = o.domain + +""" + function (o::BinaryOperation{T,D})(t1::T, t2::T) where {T<:Truth, D<:AbstractSet{T}} + +Helper allowing to use binary operations with function notation. + +See also [`Operation`](@ref), [`BinaryOperation`](@ref), [`arity`](@ref). +""" +function (o::BinaryOperation{T,D})(t1::T, t2::T) where {T<:Truth, D<:AbstractSet{T}} + return o.truthtable[(t1, t2)] +end diff --git a/src/many-valued-logics/order-utilities.jl b/src/many-valued-logics/order-utilities.jl new file mode 100644 index 00000000..3eb551f2 --- /dev/null +++ b/src/many-valued-logics/order-utilities.jl @@ -0,0 +1,117 @@ +""" + function precedeq( + l::L, + t1::T, + t2::T + ) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} + } + +Return true if `t1` ≤ `t2` in `l`. Given an algebraically defined lattice (L, ∨, ∧), one can +define a partial order ≤ on L by setting a ≤ b if a = a ∧ b. + +See also [`precedes`](@ref), [`succeedes`](@ref), [`succeedeq`](@ref). +""" +function precedeq( + l::L, + t1::T, + t2::T +) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} +} + !islattice(l) && error("Cannot convert object of type $(typeof(l)) to an object of " * + "type FiniteLattice.") + if l.meet(t1, t2) == t1 + return true + else + return false + end +end + +""" + function precedes( + l::L, + t1::T, + t2::T + ) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} + } + +Return true if `t1` < `t2` in `l`. Given an algebraically defined lattice (L, ∨, ∧), one can +define a partial order ≤ on L by setting a ≤ b if a = a ∧ b. + +See also [`precedeq`](@ref), [`succeedes`](@ref), [`succeedeq`](@ref). +""" +function precedes( + l::L, + t1::T, + t2::T +) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} +} + t1 != t2 && precedeq(l, t1, t2) +end + +""" + function succeedeq( + l::L, + t1::T, + t2::T + ) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} + } + +Return true if `t1` ≥ `t2` in `l`. Given an algebraically defined lattice (L, ∨, ∧), one can +define a partial order ≤ on L by setting a ≤ b if a = a ∧ b. + +See also [`precedes`](@ref), [`precedeq`](@ref), [`succeedes`](@ref). +""" +function succeedeq( + l::L, + t1::T, + t2::T +) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} +} + precedeq(l, t2, t1) +end + +""" + function succeedeq( + l::L, + t1::T, + t2::T + ) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} + } + +Return true if `t1` > `t2` in `l`. Given an algebraically defined lattice (L, ∨, ∧), one can +define a partial order ≤ on L by setting a ≤ b if a = a ∧ b. + +See also [`precedes`](@ref), [`precedeq`](@ref), [`succeedeq`](@ref). +""" +function succeedes( + l::L, + t1::T, + t2::T +) where { + T<:Truth, + D<:AbstractSet{T}, + L<:FiniteAlgebra{T,D} +} + precedes(l, t2, t1) +end diff --git a/src/modal-logic.jl b/src/modal-logic.jl index 4d549371..3346c0f5 100644 --- a/src/modal-logic.jl +++ b/src/modal-logic.jl @@ -303,10 +303,128 @@ See also """ isgrounding(::AbstractRelation) = false -include("algebras/relations.jl") +############################################################################################ +############################################################################################ +############################################################################################ + +############################################################################################ +# Singletons representing natural relations +############################################################################################ + +doc_identityrel = """ + struct IdentityRel <: AbstractRelation end; + const identityrel = IdentityRel(); + +Singleton type for the identity relation. This is a binary relation via which a world +accesses itself. The relation is also symmetric, reflexive and transitive. + +# Examples +```julia-repl +julia> syntaxstring(SoleLogics.identityrel) +"=" + +julia> SoleLogics.converse(identityrel) +IdentityRel() +``` + +See also +[`globalrel`](@ref), +[`AbstractRelation`](@ref), +[`AbstractWorld`](@ref), +[`AbstractFrame`](@ref). +[`AbstractKripkeStructure`](@ref), +""" + +"""$(doc_identityrel)""" +struct IdentityRel <: AbstractRelation end; +"""$(doc_identityrel)""" +const identityrel = IdentityRel(); + +arity(::IdentityRel) = 2 + +syntaxstring(::IdentityRel; kwargs...) = "=" + +hasconverse(::IdentityRel) = true +converse(::IdentityRel) = identityrel +istoone(::IdentityRel) = true +issymmetric(::IdentityRel) = true +isreflexive(::IdentityRel) = true +istransitive(::IdentityRel) = true + +############################################################################################ + +doc_globalrel = """ + struct GlobalRel <: AbstractRelation end; + const globalrel = GlobalRel(); + +Singleton type for the global relation. This is a binary relation via which a world +accesses every other world within the frame. +The relation is also symmetric, reflexive and transitive. + +# Examples +```julia-repl +julia> syntaxstring(SoleLogics.globalrel) +"G" + +julia> SoleLogics.converse(globalrel) +GlobalRel() +``` + +See also +[`identityrel`](@ref), +[`AbstractRelation`](@ref), +[`AbstractWorld`](@ref), +[`AbstractFrame`](@ref). +[`AbstractKripkeStructure`](@ref), +""" + +"""$(doc_globalrel)""" +struct GlobalRel <: AbstractRelation end; +"""$(doc_globalrel)""" +const globalrel = GlobalRel(); + +arity(::GlobalRel) = 2 + +syntaxstring(::GlobalRel; kwargs...) = "G" + +hasconverse(::GlobalRel) = true +converse(::GlobalRel) = globalrel +issymmetric(::GlobalRel) = true +isreflexive(::GlobalRel) = true +istransitive(::GlobalRel) = true +isgrounding(::GlobalRel) = true ############################################################################################ +""" +A binary relation via which a world *is accessed* by every other world within the frame. +That is, the binary relation that leads to a world. + +See also +[`identityrel`](@ref), +[`AbstractRelation`](@ref), +[`AbstractWorld`](@ref), +[`AbstractFrame`](@ref). +[`AbstractKripkeStructure`](@ref), +""" +struct AtWorldRelation{W<:AbstractWorld} <: AbstractRelation + w::W +end; + +arity(::AtWorldRelation) = 2 + +syntaxstring(r::AtWorldRelation; kwargs...) = "@($(syntaxstring(r.w)))" + +hasconverse(::AtWorldRelation) = false +issymmetric(::AtWorldRelation) = false +isreflexive(::AtWorldRelation) = false +istransitive(::AtWorldRelation) = true +isgrounding(::AtWorldRelation) = true + +############################################################################################ +############################################################################################ +############################################################################################ + """ abstract type AbstractMultiModalFrame{W<:AbstractWorld} <: AbstractFrame{W} end @@ -375,7 +493,7 @@ that are, then, fed to the world constructor the using IterTools generators, as As such, when defining new frames, worlds, and/or relations, one should provide new methods for `_accessibles`. For example: - _accessibles(fr::Full1DFrame, w::Interval{Int}, ::_IA_A) = zip(Iterators.repeated(w.y), w.y+1:X(fr)+1) + _accessibles(fr::Full1DFrame, w::Interval{<:Integer}, ::_IA_A) = zip(Iterators.repeated(w.y), w.y+1:X(fr)+1) This pattern is generally convenient; it can, however, be bypassed, although this requires defining two additional methods in order to @@ -417,7 +535,7 @@ See also [`AbstractWorld`](@ref), [`AbstractRelation`](@ref), [`AbstractMultiModalFrame`](@ref). """ function accessibles( - fr::AbstractMultiModalFrame{W}, + fr::AbstractMultiModalFrame, w::W, r::AbstractRelation ) where {W<:AbstractWorld} @@ -484,6 +602,9 @@ end # nworlds(fr::AdjMatMultiModalFrame) = length(fr) + +include("algebras/relations.jl") + include("algebras/frames.jl") ############################################################################################ @@ -975,18 +1096,26 @@ ismodal(::Type{<:BoxRelationalConnective}) = true isbox(::Type{<:DiamondRelationalConnective}) = false isbox(::Type{<:BoxRelationalConnective}) = true -function syntaxstring(op::DiamondRelationalConnective; use_modal_superscript_notation = false, kwargs...) - if use_modal_superscript_notation +function syntaxstring(op::DiamondRelationalConnective; use_modal_notation = nothing, kwargs...) + if isnothing(use_modal_notation) + return "⟨$(syntaxstring(relation(op); kwargs...))⟩" + elseif use_modal_notation == :superscript return "◊$(SoleBase.superscript(syntaxstring(relation(op); kwargs...)))" + # elseif use_modal_notation == :subscript + # return "◊$(SoleBase.subscript(syntaxstring(relation(op); kwargs...)))" else - return "⟨$(syntaxstring(relation(op); kwargs...))⟩" + return error("Unexpected value for parameter `use_modal_notation`. Allowed are: [nothing, :superscript]") end end -function syntaxstring(op::BoxRelationalConnective; use_modal_superscript_notation = false, kwargs...) - if use_modal_superscript_notation +function syntaxstring(op::BoxRelationalConnective; use_modal_notation = nothing, kwargs...) + if isnothing(use_modal_notation) + return "[$(syntaxstring(relation(op); kwargs...))]" + elseif use_modal_notation == :superscript return "□$(SoleBase.superscript(syntaxstring(relation(op); kwargs...)))" + # elseif use_modal_notation == :subscript + # return "□$(SoleBase.subscript(syntaxstring(relation(op); kwargs...)))" else - return "[$(syntaxstring(relation(op); kwargs...))]" + return error("Unexpected value for parameter `use_modal_notation`. Allowed are: [nothing, :superscript]") end end diff --git a/src/old-code/many-valued-logics/flew-algebras.jl b/src/old-code/many-valued-logics/flew-algebras.jl new file mode 100644 index 00000000..deb92aaa --- /dev/null +++ b/src/old-code/many-valued-logics/flew-algebras.jl @@ -0,0 +1,143 @@ +using ..SoleLogics: AbstractAlgebra +import ..SoleLogics: syntaxstring +import Base: convert + +struct FLewTruth <: Truth + label::String + + function FLewTruth(label::String) + return new(label) + end + + function FLewTruth(t::BooleanTruth) + return convert(FLewTruth, t) + end +end + +syntaxstring(t::FLewTruth; kwargs...) = t.label +convert(::Type{FLewTruth}, t::BooleanTruth) = istop(t) ? FLewTruth("⊤") : FLewTruth("⊥") + +""" + struct FLewAlgebra <: AbstractAlgebra{FLewTruth} + domain::Set{FLewTruth} + jointable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth} + meettable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth} + monoidtable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth} + implicationtable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth} + bot::FLewTruth + top::FLewTruth + end + +An FLew-algebra is an algebra (L, ∨, ∧, ⋅, →, ⊥, ⊤), where + - (L, ∨, ∧, ⊥, ⊤) is a lattice with top element ⊤ and bottom element ⊥ + - (L, ⋅, ⊤) is a commutative monoid + - The residuation property holds: x ⋅ y ≤ z iff x ≤ y → z + +A lattice is an algebraic structure (L, ∨, ∧) consisting of a set L and two binary, +commutative and associative operations ∨ and ∧ on L satisfying the following axiomatic +identities for all elements a, b ∈ L (sometimes called absorption laws): + - a ∨ (a ∧ b) = a + - a ∧ (a ∨ b) = a + +The following two identities are also usally regarded as axioms, even though they follow +from the two absorption laws taken together. These are called idempotent laws: + - a ∨ a = a + - a ∧ a = a + +A bounded lattice is an algebraic structure (L, ∨, ∧, ⊥, ⊤) such that (L, ∨, ∧) is a +lattice, the bottom element ⊥ is the identity element for the join operation ∨, and the top +element ⊤ is the identity element for the meet operation ∧: + - a ∨ ⊥ = a + - a ∧ ⊤ = a + +A monoid (L, ⋅, e) is a set L equipped with a binary operation L × L → L, denoted as ⋅, +satisfying the following axiomatic identities: + - (Associativity) ∀ a, b, c ∈ L, the equation (a ⋅ b) ⋅ c = a ⋅ (b ⋅ c) holds. + - (Identity element) There exists an element e ∈ L such that for every element a ∈ L, the equalities e ⋅ a = a + and a ⋅ e = a hold. + +The identity element of a monoid is unique. + +A commutative monoid is a monoid whose operation is commutative. +""" +struct FLewAlgebra <: AbstractAlgebra{FLewTruth} + domain::Set{FLewTruth} + jointable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth} + meettable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth} + monoidtable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth} + implicationtable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth} + bot::FLewTruth + top::FLewTruth + + function FLewAlgebra( + domain::Set{FLewTruth}, + jointable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}, + meettable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}, + monoidtable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}, + implicationtable::Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}, + bot::FLewTruth, + top::FLewTruth + ) + for i ∈ domain + for j ∈ domain + @assert (i, j) ∈ keys(jointable) "jointable[($i, $j)] is not defined." + @assert (i, j) ∈ keys(meettable) "meettable[($i, $j)] is not defined." + @assert (i, j) ∈ keys(monoidtable) "monoidtable[($i, $j)] is not defined." + @assert (i, j) ∈ keys(monoidtable) "implicationtable[($i, $j)] is not defined." + end + end + @assert length(jointable) == length(domain)^2 "Found jointable[(i, j)] where i or j ∉ domain." + @assert length(meettable) == length(domain)^2 "Found meettable[(i, j)] where i or j ∉ domain." + @assert length(monoidtable) == length(domain)^2 "Found monoidtable[(i, j)] where i or j ∉ domain." + @assert length(implicationtable) == length(domain)^2 "Found implicationtable[(i, j)] where i or j ∉ domain." + for i ∈ domain + @assert monoidtable[(i, FLewTruth(⊤))] == i "Defined monoid don't satisfy the neutral element rule: monoidtable[($i, ⊤) ≠ $i]." + for j ∈ domain + @assert jointable[(i, j)] == jointable[(j, i)] "Defined join is not commutative: jointable[($i,$j)] ≠ jointable[($j,$i)]." + @assert meettable[(i, j)] == meettable[(j, i)] "Defined meet is not commutative: meettable[($i,$j)] ≠ meettable[($j,$i)]." + @assert monoidtable[(i, j)] == monoidtable[(j, i)] "Defined monoid is not commutative: monoidtable[($i,$j)] ≠ monoidtable[($j,$i)]." + for k ∈ domain + @assert jointable[(jointable[(i, j)], k)] == jointable[(i, jointable[(j, k)])] "Defined join is not associative: jointable[(jointable[(i, j)], k)] ≠ jointable[(i, jointable[(j, k)])]." + @assert meettable[(meettable[(i, j)], k)] == meettable[(i, meettable[(j, k)])] "Defined meet is not associative: meettable[(meettable[(i, j)], k)] ≠ meettable[(i, meettable[(j, k)])]." + @assert monoidtable[(monoidtable[(i,j)], k)] == monoidtable[(i, monoidtable[(j, k)])] "Defined monoid is not associative: monoidtable[(monoidtable[(i,j)], k)] ≠ monoidtable[(i, monoidtable[(j, k)])]." + end + @assert jointable[(i, meettable[(i, j)])] == i "Defined join and meet don't satisfy the asborption law: jointable[($i, meettable[($i, $j)])] ≠ $i." + @assert meettable[(i, jointable[(i, j)])] == i "Defined join and meet don't satisfy the asborption law: meettable[($i, jointable[($i, $j)])] ≠ $i." + end + @assert jointable[(i, i)] == i "Defined join don't satisfy the idempotent law: jointable[($i, $i) ≠ $i]." + @assert meettable[(i, i)] == i "Defined meet don't satisfy the idempotent law: meettable[($i, $i) ≠ $i]." + @assert meettable[(bot, i)] == bot "$bot isn't a valid bottom element: $bot ≰ $i" + @assert jointable[(i, top)] == top "$top isn't a valid top element: $i ≰ $top" + end + return new(domain, meettable, jointable, monoidtable, implicationtable, bot, top) + end +end + +join(a::FLewAlgebra, t1::FLewTruth, t2::FLewTruth) = a.jointable[(t1, t2)] +meet(a::FLewAlgebra, t1::FLewTruth, t2::FLewTruth) = a.meettable[(t1, t2)] +monoid(a::FLewAlgebra, t1::FLewTruth, t2::FLewTruth) = a.monoidtable[(t1, t2)] +implication(a::FLewAlgebra, t1::FLewTruth, t2::FLewTruth) = a.implicationtable[(t1, t2)] +isbot(a::FLewAlgebra, t::FLewTruth) = t == a.bot +itop(a::FLewAlgebra, t::FLewTruth) = t == a.top + +""" + precedes(a::FLewAlgebra, t1::FLewTruth, t2::FLewTruth) + +Given an algebraically defined lattice (L, ∨, ∧), one can define a partial ordern ≤ on L by +setting: + - a ≤ b if a = a ∧ b, or + - a ≤ b if b = a ∨ b, + +for all elements a, b ∈ L. The laws of absorption ensure that both definitions are +equivalent: + - a = a ∧ b implies b = b ∨ (b ∧ a) = (a ∧ b) ∨ b = a ∨ b + +and dually for the other direction. +""" +function precedes(a::FLewAlgebra, t1::FLewTruth, t2::FLewTruth) + if meet(a, t1, t2) == t1 + return true + else + return false + end +end diff --git a/src/fuzzy.jl b/src/old-code/many-valued-logics/heyting-algebras.jl similarity index 95% rename from src/fuzzy.jl rename to src/old-code/many-valued-logics/heyting-algebras.jl index 86f0fa35..ae2985f2 100644 --- a/src/fuzzy.jl +++ b/src/old-code/many-valued-logics/heyting-algebras.jl @@ -1,4 +1,6 @@ using Graphs +using ..SoleLogics: AbstractAlgebra +import ..SoleLogics: istop, simplify # Author: alberto-paparella @@ -103,8 +105,8 @@ struct HeytingAlgebra{ graph::G # directed graph where (α, β) represents α ≺ β transitiveclosure::G # transitive closure of the graph (useful for some optimization) isevaluated::Bool - meet::Vector{Vector{HeytingTruth}} - join::Vector{Vector{HeytingTruth}} + meettable::Vector{Vector{HeytingTruth}} + jointable::Vector{Vector{HeytingTruth}} implication::Vector{Vector{HeytingTruth}} maxmembers::Vector{Vector{HeytingTruth}} minmembers::Vector{Vector{HeytingTruth}} @@ -126,23 +128,23 @@ struct HeytingAlgebra{ "with a graph which is not a complete lattice." if evaluate tc = transitiveclosure(graph) - meet = [Vector{HeytingTruth}(undef, length(domain)) for _ in 1:length(domain)] - join = [Vector{HeytingTruth}(undef, length(domain)) for _ in 1:length(domain)] + meettable = [Vector{HeytingTruth}(undef, length(domain)) for _ in 1:length(domain)] + jointable = [Vector{HeytingTruth}(undef, length(domain)) for _ in 1:length(domain)] implication = [Vector{HeytingTruth}(undef, length(domain)) for _ in 1:length(domain)] maxmembers = Vector{Vector{HeytingTruth}}(undef, length(domain)) minmembers = Vector{Vector{HeytingTruth}}(undef, length(domain)) for α ∈ domain for β ∈ domain - meet[index(α)][index(β)] = greatestlowerbound(domain, tc, α, β) - join[index(α)][index(β)] = leastupperbound(domain, tc, α, β) + meettable[index(α)][index(β)] = greatestlowerbound(domain, tc, α, β) + jointable[index(α)][index(β)] = leastupperbound(domain, tc, α, β) end end for α ∈ domain for β ∈ domain η = HeytingTruth(⊥) for γ ∈ domain - if precedeq(domain, tc, meet[index(α)][index(γ)], β) - η = join[index(η)][index(γ)] + if precedeq(domain, tc, meettable[index(α)][index(γ)], β) + η = jointable[index(η)][index(γ)] end end implication[index(α)][index(β)] = η @@ -152,7 +154,7 @@ struct HeytingAlgebra{ maxmembers[index(α)] = maximalmembers(domain, tc, α) minmembers[index(α)] = minimalmembers(domain, tc, α) end - return new{D,G}(domain, graph, tc, true, meet, join, implication, maxmembers, minmembers) + return new{D,G}(domain, graph, tc, true, meettable, jointable, implication, maxmembers, minmembers) else return new{D,G}(domain, graph, transitiveclosure(graph), false) end @@ -170,11 +172,11 @@ graph(h::HeytingAlgebra) = h.graph Graphs.transitiveclosure(h::HeytingAlgebra) = h.transitiveclosure isevaluated(h::HeytingAlgebra) = h.isevaluated -meet(h::HeytingAlgebra) = h.meet +meet(h::HeytingAlgebra) = h.meettable meet(h::HeytingAlgebra, α, β) = meet(h)[index(α)][index(β)] -Base.join(h::HeytingAlgebra) = h.join -Base.join(h::HeytingAlgebra, α, β) = join(h)[index(α)][index(β)] +join(h::HeytingAlgebra) = h.jointable +join(h::HeytingAlgebra, α, β) = join(h)[index(α)][index(β)] implication(h::HeytingAlgebra) = h.implication implication(h::HeytingAlgebra, α, β) = implication(h)[index(α)][index(β)] diff --git a/src/syntax-utils.jl b/src/syntax-utils.jl index 5a1b8f3b..3e5dbe1d 100644 --- a/src/syntax-utils.jl +++ b/src/syntax-utils.jl @@ -34,6 +34,23 @@ LeftmostLinearForm{SoleLogics.NamedConnective{:∨},Literal} julia> LeftmostDisjunctiveForm([LeftmostConjunctiveForm(parseformula.(["¬p", "q", "¬r"]))]) isa DNF true +julia> conj = LeftmostConjunctiveForm(@atoms p q) +LeftmostConjunctiveForm with 2 Atom{String} children: + p + q + +julia> tree(conj) +SyntaxBranch{NamedConnective{:∧}}: p ∧ q + +julia> nconj = NEGATION(conj) +LeftmostLinearForm with connective ¬ and 1 LeftmostConjunctiveForm{Atom{String}} children: + (p) ∧ (q) + +julia> tree(nconj) +SyntaxBranch{NamedConnective{:¬}}: ¬(p ∧ q) + +julia> tree(nconj ∧ nconj) +SyntaxBranch{NamedConnective{:∧}}: ¬(p ∧ q) ∧ ¬(p ∧ q) ``` """ @@ -181,9 +198,12 @@ function tree(lf::LeftmostLinearForm) chs = children(lf) st = begin - if length(chs) == 1 - # Only child - tree(first(chs)) + if length(chs) == 1 # Only child + if a == 1 + c(tree(first(chs))) + else + tree(first(chs)) + end else function _tree(φs::Vector{<:SyntaxTree}) @assert (length(φs) != 0) "$(φs); $(lf); $(c); $(a)." @@ -228,6 +248,9 @@ Base.promote_rule(::Type{<:LeftmostLinearForm}, ::Type{<:LeftmostLinearForm}) = Base.promote_rule(::Type{SS}, ::Type{LF}) where {SS<:AbstractSyntaxStructure,LF<:LeftmostLinearForm} = SyntaxTree Base.promote_rule(::Type{LF}, ::Type{SS}) where {LF<:LeftmostLinearForm,SS<:AbstractSyntaxStructure} = SyntaxTree +Base.promote_rule(::Type{LF}, ::Type{SS}) where {LF<:LeftmostLinearForm,SS<:SyntaxTree} = SyntaxTree +Base.promote_rule(::Type{SS}, ::Type{LF}) where {LF<:LeftmostLinearForm,SS<:SyntaxTree} = SyntaxTree + ############################################################################################ # TODO actually: diff --git a/test/algebras/relations.jl b/test/algebras/relations.jl index a43b5cfe..dd4e8069 100644 --- a/test/algebras/relations.jl +++ b/test/algebras/relations.jl @@ -1,52 +1,153 @@ +using Test using FunctionWrappers using FunctionWrappers: FunctionWrapper using SoleLogics -using SoleLogics: FunctionalWorldFilter +using SoleLogics: FullDimensionalFrame, allworlds +using SoleLogics: FunctionalWorldFilter, IntervalLengthFilter +using SoleLogics: filterworlds, FilteredRelation +using SoleLogics: IA7Relations, IA3Relations, IARelations_extended +using BenchmarkTools -f1(i::Interval{Int})::Bool = true -fw = FunctionWrapper{Bool, Tuple{Interval{Int}}}(f1) -i = Interval{Int}(1,2) +f1(i::Interval{Int})::Bool = length(i) ≥ 3 +funcw = FunctionWrapper{Bool,Tuple{Interval{Int}}}(f1) +fr = SoleLogics.FullDimensionalFrame(10) +myworlds = SoleLogics.allworlds(fr) -fwf = FunctionalWorldFilter{Interval{Int}, typeof(f1)}(fw) -@test fwf.filter(i) == true -@test_throws MethodError fwf.filter(2) +wf = FunctionalWorldFilter{Interval{Int},typeof(f1)}(funcw) +@test length(collect(filterworlds(wf, myworlds))) == 36 +@test_throws MethodError collect(filterworlds(wf, [2])) -fwf = FunctionalWorldFilter{Interval{Int}}(fw, typeof(f1)) -@test fwf.filter(i) == true -@test_throws MethodError fwf.filter(2) +wf = FunctionalWorldFilter{Interval{Int}}(funcw, typeof(f1)) +@test length(collect(filterworlds(wf, myworlds))) == 36 +@test_throws MethodError collect(filterworlds(wf, [2])) -fwf = FunctionalWorldFilter(fw, typeof(f1)) -@test fwf.filter(i) == true -@test_throws MethodError fwf.filter(2) +wf = FunctionalWorldFilter(funcw, typeof(f1)) +@test length(collect(filterworlds(wf, myworlds))) == 36 +@test_throws MethodError collect(filterworlds(wf, [2])) -@test_logs ( - :warn, - "FunctionalWorldFilter initialized without specifying the functiontype.\n"* - "Please consider using the following syntax instead:\n"* - " FunctionalWorldFilter(FunctionWrapper{Bool, Tuple{W}}(filter), typeof(filter))\n"* - "where W is a subtype of AbstractWorld and filter is a Function." -) fwf = FunctionalWorldFilter(fw) -@test fwf.filter(i) == true -@test_throws MethodError fwf.filter(2) - -fwf = FunctionalWorldFilter{Interval{Int}, typeof(f1)}(f1) -@test fwf.filter(i) == true -@test_throws MethodError fwf.filter(2) - -fwf = FunctionalWorldFilter{Interval{Int}}(f1) -@test fwf.filter(i) == true -@test_throws MethodError fwf.filter(2) - -fwf = FunctionalWorldFilter(f1, Interval{Int}) -@test fwf.filter(i) == true -@test_throws MethodError fwf.filter(2) +wf_lf = IntervalLengthFilter(≥, 3) +@test length(collect(filterworlds(wf_lf, myworlds))) == 36 +@test_nowarn collect(filterworlds(wf_lf, [2])) # Warn abouth this behavior!! + +bigfr = SoleLogics.FullDimensionalFrame(40) +collect(accessibles(bigfr, Interval(1, 2), IA_L)) +collect(accessibles(bigfr, Interval(1, 2), FilteredRelation(IA_L, wf))) +collect(accessibles(bigfr, Interval(1, 2), FilteredRelation(IA_L, wf_lf))) + +@test_logs ( :warn, ) wf = FunctionalWorldFilter(funcw) +@test length(collect(filterworlds(wf, myworlds))) == 36 +@test_throws MethodError collect(filterworlds(wf, [2])) + +wf = FunctionalWorldFilter{Interval{Int},typeof(f1)}(f1) +@test length(collect(filterworlds(wf, myworlds))) == 36 +@test_throws MethodError collect(filterworlds(wf, [2])) + +wf = FunctionalWorldFilter{Interval{Int}}(f1) +@test length(collect(filterworlds(wf, myworlds))) == 36 +@test_throws MethodError collect(filterworlds(wf, [2])) + +wf = FunctionalWorldFilter(f1, Interval{Int}) +@test length(collect(filterworlds(wf, myworlds))) == 36 +@test_throws MethodError collect(filterworlds(wf, [2])) @test_logs ( :warn, - "FunctionalWorldFilter initialized without specifying the worldtype.\n"* - "Plese consider using the following syntax instead:\n"* - " FunctionalWorldFilter(filter, worldtype)\n"* + "FunctionalWorldFilter initialized without specifying the worldtype.\n" * + "Plese consider using the following syntax instead:\n" * + " FunctionalWorldFilter(filter, worldtype)\n" * "where worldtype is a subtype of AbstractWorld and filter is a Function." -) fwf = FunctionalWorldFilter(f1) -@test fwf.filter(i) == true -@test_throws MethodError fwf.filter(2) +) wf = FunctionalWorldFilter(f1) +@test length(collect(filterworlds(wf, myworlds))) == 36 +@test_throws MethodError collect(filterworlds(wf, [2])) + +@test collect(accessibles( + fr, + first(allworlds(fr)), + FilteredRelation(globalrel, wf) +)) == collect(accessibles( + fr, + first(allworlds(fr)), + FilteredRelation(globalrel, wf_lf) +)) + +fr = FullDimensionalFrame(20) +worlds = allworlds(fr) +operators = [≤, ≥, ==] + + +for r in union(IARelations_extended, IA7Relations, IA3Relations) + # @show r + for w in worlds + for o in operators + for l in 1:21 + @test all(((x,y),)->x == y, zip(accessibles( + fr, + w, + FilteredRelation(r, FunctionalWorldFilter{Interval}(i->o(i.y-i.x, l))) + ),accessibles( + fr, + w, + FilteredRelation(r, IntervalLengthFilter(o, l)) + ))) + end + end + end +end + + +# for r in IARelations_extended +# for w in worlds +# # for r in union(IARelations_extended, IA7Relations, IA3Relations) +# for o in operators +# for l in 1:21 +# @test collect(accessibles( +# fr, +# w, +# FilteredRelation(r, FunctionalWorldFilter{Interval}(i->o(i.y-i.x, l))) +# )) == collect(accessibles( +# fr, +# w, +# FilteredRelation(r, IntervalLengthFilter(o, l)) +# )) +# end +# end +# end +# end + +# for r in IA7Relations +# # @show r +# for w in worlds +# for o in operators +# for l in 1:21 +# @test collect(accessibles( +# fr, +# w, +# FilteredRelation(r, FunctionalWorldFilter{Interval}(i->o(i.y-i.x, l))) +# )) == collect(accessibles( +# fr, +# w, +# FilteredRelation(r, IntervalLengthFilter(o, l)) +# )) +# end +# end +# end +# end + +# for r in IA3Relations +# # @show r +# for w in worlds +# for o in operators +# for l in 1:21 +# @test collect(accessibles( +# fr, +# w, +# FilteredRelation(r, FunctionalWorldFilter{Interval}(i->o(i.y-i.x, l))) +# )) == collect(accessibles( +# fr, +# w, +# FilteredRelation(r, IntervalLengthFilter(o, l)) +# )) +# end +# end +# end +# end diff --git a/test/core.jl b/test/core.jl index a0cc1208..80d2df63 100644 --- a/test/core.jl +++ b/test/core.jl @@ -273,11 +273,12 @@ emptylogic = @test_nowarn propositionallogic(; operators = SoleLogics.Operator[] @test syntaxstring(SoleLogics._Topo_TPPi()) == "T̅P̅P̅" @test syntaxstring(diamond(IA_A)) == "⟨A⟩" -@test syntaxstring(diamond(IA_A); use_modal_superscript_notation=true) == "◊ᴬ" -@test syntaxstring(diamond(IA_A); use_modal_superscript_notation=false) == "⟨A⟩" -@test syntaxstring(diamond(IA_A); use_modal_superscript_notation=true) != syntaxstring(diamond(IA_A)(⊤); use_modal_superscript_notation=false) +@test syntaxstring(diamond(IA_A); use_modal_notation=:superscript) == "◊ᴬ" +@test syntaxstring(diamond(IA_A); use_modal_notation=nothing) == "⟨A⟩" +@test syntaxstring(diamond(IA_A); use_modal_notation=:superscript) != syntaxstring(diamond(IA_A)(⊤); use_modal_notation=nothing) -@test syntaxstring(diamond(SoleLogics._Topo_TPPi()); use_modal_superscript_notation=true) == "◊ᵀ̅ᴾ̅ᴾ̅" +@test syntaxstring(diamond(SoleLogics._Topo_TPPi()); use_modal_notation=:superscript) == "◊ᵀ̅ᴾ̅ᴾ̅" +@test_broken syntaxstring(diamond(SoleLogics._Topo_TPPi()); use_modal_notation=:subscript) == "◊TODO" # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/test/many-valued-logics.jl b/test/many-valued-logics.jl new file mode 100644 index 00000000..febf8a2e --- /dev/null +++ b/test/many-valued-logics.jl @@ -0,0 +1,84 @@ +using SoleLogics +using SoleLogics.ManyValuedLogics +using SoleLogics.ManyValuedLogics: Operation + +############################################################################################ +#### Operations ############################################################################ +############################################################################################ + +struct MyOperation <: Operation end + +@test_logs (:warn,) string(MyOperation()) +function Base.show(io::IO, o::MyOperation) + print(io, "MyOperation") +end +@test_throws ErrorException arity(MyOperation()) + +domain = Set{BooleanTruth}([⊥, ⊤]) +jointable = Dict{Tuple{BooleanTruth, BooleanTruth}, BooleanTruth}( + (⊥, ⊥) => ⊥, (⊥, ⊤) => ⊤, + (⊤, ⊥) => ⊤, (⊤, ⊤) => ⊤ +) +join = BinaryOperation(domain, jointable) + +@test string(join) == string(jointable) +@test arity(join) == 2 + +############################################################################################ +#### Finite algebras (boolean case) ######################################################## +############################################################################################ + +α = FiniteTruth("α") +@test string(α) == "α" + +meettable = Dict{Tuple{BooleanTruth, BooleanTruth}, BooleanTruth}( + (⊥, ⊥) => ⊥, (⊥, ⊤) => ⊥, + (⊤, ⊥) => ⊥, (⊤, ⊤) => ⊤ +) +meet = BinaryOperation(domain, meettable) +fa = FiniteLattice(join, meet) +fba = FiniteBoundedLattice(join, meet, ⊥, ⊤) + +meetmonoid = CommutativeMonoid(meet, ⊤) +frl = FiniteResiduatedLattice(join, meet, meetmonoid, ⊥, ⊤) + +ffa = FiniteFLewAlgebra(join, meet, meetmonoid, ⊥, ⊤) +@test ffa.implication(⊥, ⊥) == ⊤ +@test ffa.implication(⊥, ⊤) == ⊤ +@test ffa.implication(⊤, ⊥) == ⊥ +@test ffa.implication(⊤, ⊤) == ⊤ + +implicationtable = Dict{Tuple{BooleanTruth, BooleanTruth}, BooleanTruth}( + (⊥, ⊥) => ⊤, + (⊥, ⊤) => ⊤, + (⊤, ⊥) => ⊥, + (⊤, ⊤) => ⊤ +) +implication = BinaryOperation(domain, implicationtable) +fha = FiniteHeytingAlgebra(join, meet, implication, ⊥, ⊤) + +############################################################################################ +#### Three-valued algebra (Łukasiewich norm case) ########################################## +############################################################################################ + +d3 = Set{FiniteTruth}([⊥, α, ⊤]) +jt3 = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}( + (⊥, ⊥) => ⊥, (⊥, α) => α, (⊥, ⊤) => ⊤, + (α, ⊥) => α, (α, α) => α, (α, ⊤) => ⊤, + (⊤, ⊥) => ⊤, (⊤, α) => ⊤, (⊤, ⊤) => ⊤ +) +j3 = BinaryOperation(d3, jt3) +mt3 = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}( + (⊥, ⊥) => ⊥, (⊥, α) => ⊥, (⊥, ⊤) => ⊥, + (α, ⊥) => ⊥, (α, α) => α, (α, ⊤) => α, + (⊤, ⊥) => ⊥, (⊤, α) => α, (⊤, ⊤) => ⊤ +) +m3 = BinaryOperation(d3, mt3) +lot3 = Dict{Tuple{FiniteTruth, FiniteTruth}, FiniteTruth}( + (⊥, ⊥) => ⊥, (⊥, α) => ⊥, (⊥, ⊤) => ⊥, + (α, ⊥) => ⊥, (α, α) => ⊥, (α, ⊤) => α, + (⊤, ⊥) => ⊥, (⊤, α) => α, (⊤, ⊤) => ⊤ +) +lo3 = BinaryOperation(d3, lot3) +l3 = CommutativeMonoid(lo3, ⊤) +ffa3 = FiniteFLewAlgebra(j3, m3, l3, ⊥, ⊤) diff --git a/test/misc.jl b/test/misc.jl index 9b6e26c5..ef76916d 100644 --- a/test/misc.jl +++ b/test/misc.jl @@ -1,14 +1,141 @@ -using SoleLogics using Test +using SoleLogics + +const SL = SoleLogics # SL.name to reference unexported names + +# The following test set is intended to test the new type hierarchy update, +# considering both trivial and complex assertions regarding various aspects of SoleLogics. + +############################################################################################ +#### Declaration section ################################################################### +############################################################################################ + +p = Atom("p") +q = Atom("q") +r = Atom("r") +m = Atom(1) +n = Atom(2) + +pandq = SyntaxTree(CONJUNCTION, (p,q)) +pandq_demorgan = DISJUNCTION(p |> NEGATION, q |> NEGATION) |> NEGATION +qandp = SyntaxTree(CONJUNCTION, (q,p)) +pandr = SyntaxTree(CONJUNCTION, (p,r)) +porq = SyntaxTree(DISJUNCTION, (p,q)) +norm = SyntaxTree(DISJUNCTION, (m,n)) +trees_implication = SyntaxTree(IMPLICATION, (pandq, porq)) + +interp1 = TruthDict([p => TOP, q => TOP]) +interp2 = TruthDict(1:4, BOT) + +############################################################################################ +#### Test section ########################################################################## +############################################################################################ + +@test Formula <: Syntactical +@test AbstractSyntaxStructure <: Formula +@test SyntaxLeaf <: AbstractSyntaxStructure +@test Truth <: SyntaxLeaf + +@test TOP isa Truth +@test TOP isa BooleanTruth +@test BOT isa Truth +@test BOT isa BooleanTruth + +@test Connective <: Syntactical +@test NamedConnective <: Connective + +@test Connective <: Operator +@test Truth <: Operator +@test Connective <: SyntaxToken +@test SyntaxLeaf <: SyntaxToken + +@test SyntaxTree <: AbstractSyntaxStructure +@test SyntaxBranch <: SyntaxTree + +@test NEGATION isa NamedConnective +@test CONJUNCTION isa NamedConnective +@test DISJUNCTION isa NamedConnective +@test IMPLICATION isa NamedConnective +@test typeof(¬) <: NamedConnective +@test typeof(∧) <: NamedConnective +@test typeof(∨) <: NamedConnective +@test typeof(→) <: NamedConnective + +@test isnullary(p) == true +@test syntaxstring(p) == "p" + +@test pandq |> syntaxstring == CONJUNCTION(p, q) |> syntaxstring +@test pandq |> syntaxstring == (@synexpr p ∧ q) |> syntaxstring +@test porq |> syntaxstring == DISJUNCTION(p, q) |> syntaxstring +@test porq |> syntaxstring == (@synexpr p ∨ q) |> syntaxstring +@test trees_implication |> syntaxstring == IMPLICATION(pandq, porq) |> syntaxstring +@test trees_implication |> syntaxstring == (@synexpr pandq → porq) |> syntaxstring + +@test pandq |> syntaxstring == + SL.composeformulas(CONJUNCTION, (p, q)) |> syntaxstring +@test porq |> syntaxstring == + SL.composeformulas(DISJUNCTION, (p, q)) |> syntaxstring +@test trees_implication |> syntaxstring == + SL.composeformulas(IMPLICATION, (pandq, porq)) |> syntaxstring + +@test parseformula("p → q ∧ r") == (@synexpr p → q ∧ r) +@test parseformula("p → (q → r)") == (@synexpr p → (q → r)) +@test parseformula("p → (q ∧ r)") == (@synexpr p → (q ∧ r)) + +@test istop(@synexpr ⊤) +@test @synexpr ⊤ == TOP +@test isbot(@synexpr ⊥) +@test @synexpr ⊥ == ⊥ +@test @synexpr ⊤ ∧ ⊥ == SyntaxBranch(∧, ⊤, ⊥) +@test @synexpr ⊤ ∧ ⊥ == parseformula("⊤ ∧ ⊥") +@test @synexpr ¬⊤ == SyntaxBranch(¬, ⊤) +@test @synexpr ¬⊤ == parseformula("¬⊤") + +@test all(t -> t isa BooleanTruth, truths(@synexpr ¬⊤ → ⊥ ∨ ⊤)) + +@test normalize(@synexpr ¬⊤ → ⊥) == ⊤ +@test normalize(@synexpr ¬⊥ → ⊥) == ⊥ +@test normalize(@synexpr ⊤ ∧ ¬ ⊤) == ⊥ +@test normalize(@synexpr ⊤∧¬⊤) == ⊥ + +@test syntaxstring((@synexpr □(□(□(p))) ∧ q)) == syntaxstring(parseformula("□□□p ∧ q")) +@test syntaxstring((@synexpr □(p) ∧ q)) == syntaxstring(parseformula("□p ∧ q")) + +@test syntaxstring((@synexpr p ∧ □(□(□(q))))) == syntaxstring(parseformula("p ∧ □□□q")) +@test syntaxstring((@synexpr p ∧ □(q))) == syntaxstring(parseformula("p ∧ □q")) + +@test syntaxstring((@synexpr □(□(□(p))) → q)) == syntaxstring(parseformula("□□□p → q")) +@test syntaxstring((@synexpr □(p) → q)) == syntaxstring(parseformula("□p → q")) + +@test syntaxstring((@synexpr p → □(□(□(q))))) == syntaxstring(parseformula("p → □□□q")) +@test syntaxstring((@synexpr p → □(q))) == syntaxstring(parseformula("p → □q")) + +@test natoms(pandq) == 2 +@test natoms(trees_implication) == natoms(pandq) + natoms(porq) +@test Set(atoms(pandq)) == Set(atoms(qandp)) +@test Set(atoms(pandq)) == Set(atoms(porq)) +@test Set(atoms(pandq)) != Set(atoms(pandr)) +@test height(trees_implication) == height(pandq) + height(qandp) + +@test isequal(p, p) == true +@test isequal(p, q) == false +@test isequal(pandq, porq) == false +@test isequal(porq, porq) == true +@test isequal(pandq, pandq_demorgan) == false # This is not semantics, but syntax only. + +@test token(pandq) == CONJUNCTION +@test token(norm) == DISJUNCTION +@test token(pandq_demorgan) == NEGATION +@test token(trees_implication) == IMPLICATION -@test_nowarn SoleLogics.displaysyntaxvector([Atom(1)]) -# Atom{Int64}["1"] +@test trees_implication |> children |> first == pandq +@test trees_implication |> children |> last == porq -@test_nowarn SoleLogics.displaysyntaxvector([Atom(1)]; quotes = false) -# Atom{Int64}[1] +@test norm |> children |> first == SyntaxTree(m) +@test norm |> children |> first |> token == m +@test norm |> children |> first |> token |> value == value(m) -@test_nowarn SoleLogics.displaysyntaxvector(Atom.(1:20); quotes = false) -# Atom{Int64}[1, 2, 3, 4, ..., 16, 17, 18, 19, 20] +@test_nowarn interp1[p] = BOT +@test_nowarn interp1[p] = TOP -@test_nowarn SoleLogics.displaysyntaxvector(Atom.(1:20)) -# Atom{Int64}["1", "2", "3", "4", ..., "16", "17", "18", "19", "20"] +@test check(pandq, interp1) == true diff --git a/test/old-code/flew-algebras.jl b/test/old-code/flew-algebras.jl new file mode 100644 index 00000000..f5ee9faa --- /dev/null +++ b/test/old-code/flew-algebras.jl @@ -0,0 +1,74 @@ +using SoleLogics +using SoleLogics.ManyValuedLogics +using SoleLogics.ManyValuedLogics: FLewTruth, FLewAlgebra, meet, join, monoid + +⊥, α, β, γ, ⊤ = FLewTruth.(["⊥", "α", "β", "γ", "⊤"]) +domain = Set{FLewTruth}([⊥, α, β, ⊤]) + +jointable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => α, (⊥,β) => β, (⊥,⊤) => ⊤, + (α,⊥) => α, (α,α) => α, (α,β) => ⊤, (α,⊤) => ⊤, + (β,⊥) => β, (β,α) => ⊤, (β,β) => β, (β,⊤) => ⊤, + (⊤,⊥) => ⊤, (⊤,α) => ⊤, (⊤,β) => ⊤, (⊤,⊤) => ⊤, +) +meettable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => ⊥, (⊥,β) => ⊥, (⊥,⊤) => ⊥, + (α,⊥) => ⊥, (α,α) => α, (α,β) => ⊥, (α,⊤) => α, + (β,⊥) => ⊥, (β,α) => ⊥, (β,β) => β, (β,⊤) => β, + (⊤,⊥) => ⊥, (⊤,α) => α, (⊤,β) => β, (⊤,⊤) => ⊤, +) +monoidtable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => ⊥, (⊥,β) => ⊥, (⊥,⊤) => ⊥, + (α,⊥) => ⊥, (α,α) => α, (α,β) => ⊥, (α,⊤) => α, + (β,⊥) => ⊥, (β,α) => ⊥, (β,β) => β, (β,⊤) => β, + (⊤,⊥) => ⊥, (⊤,α) => α, (⊤,β) => β, (⊤,⊤) => ⊤, +) +implicationtable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => ⊤, (⊥,β) => ⊤, (⊥,⊤) => ⊤, + (α,⊥) => β, (α,α) => ⊤, (α,β) => β, (α,⊤) => α, + (β,⊥) => α, (β,α) => α, (β,β) => ⊤, (β,⊤) => β, + (⊤,⊥) => ⊥, (⊤,α) => α, (⊤,β) => β, (⊤,⊤) => ⊤, +) + +incompletejointable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => α, (⊥,β) => β, (⊥,⊤) => ⊤, + (α,⊥) => α, (α,β) => ⊤, (α,⊤) => ⊤, + (β,⊥) => β, (β,α) => ⊤, (β,β) => β, (β,⊤) => ⊤, + (⊤,⊥) => ⊤, (⊤,α) => ⊤, (⊤,β) => ⊤, (⊤,⊤) => ⊤, +) +incompletemeettable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => ⊥, (⊥,β) => ⊥, (⊥,⊤) => ⊥, + (α,⊥) => ⊥, (α,β) => ⊥, (α,⊤) => α, + (β,⊥) => ⊥, (β,α) => ⊥, (β,β) => β, (β,⊤) => β, + (⊤,⊥) => ⊥, (⊤,α) => α, (⊤,β) => β, (⊤,⊤) => ⊤, +) +incompletemonoidtable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => ⊥, (⊥,β) => ⊥, (⊥,⊤) => ⊥, + (α,⊥) => ⊥, (α,β) => ⊥, (α,⊤) => α, + (β,⊥) => ⊥, (β,α) => ⊥, (β,β) => β, (β,⊤) => β, + (⊤,⊥) => ⊥, (⊤,α) => α, (⊤,β) => β, (⊤,⊤) => ⊤, +) + +overflowingjointable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => α, (⊥,β) => β, (⊥,⊤) => ⊤, + (α,⊥) => α, (α,α) => α, (α,β) => ⊤, (α,⊤) => ⊤, + (β,⊥) => β, (β,α) => ⊤, (β,β) => β, (β,⊤) => ⊤, + (γ,⊥) => γ, + (⊤,⊥) => ⊤, (⊤,α) => ⊤, (⊤,β) => ⊤, (⊤,⊤) => ⊤, +) +overflowingmeettable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => ⊥, (⊥,β) => ⊥, (⊥,⊤) => ⊥, + (α,⊥) => ⊥, (α,α) => α, (α,β) => ⊥, (α,⊤) => α, + (β,⊥) => ⊥, (β,α) => ⊥, (β,β) => β, (β,⊤) => β, + (γ,⊥) => γ, + (⊤,⊥) => ⊥, (⊤,α) => α, (⊤,β) => β, (⊤,⊤) => ⊤, +) +overflowingmonoidtable = Dict{Tuple{FLewTruth, FLewTruth}, FLewTruth}( + (⊥,⊥) => ⊥, (⊥,α) => ⊥, (⊥,β) => ⊥, (⊥,⊤) => ⊥, + (α,⊥) => ⊥, (α,α) => α, (α,β) => ⊥, (α,⊤) => α, + (β,⊥) => ⊥, (β,α) => ⊥, (β,β) => β, (β,⊤) => β, + (γ,⊥) => γ, + (⊤,⊥) => ⊥, (⊤,α) => α, (⊤,β) => β, (⊤,⊤) => ⊤, +) + +myalgebra = FLewAlgebra(domain, jointable, meettable, monoidtable, implicationtable, ⊥, ⊤) diff --git a/test/fuzzy.jl b/test/old-code/heyting-algebras.jl similarity index 99% rename from test/fuzzy.jl rename to test/old-code/heyting-algebras.jl index 4d9c47d7..87f00193 100644 --- a/test/fuzzy.jl +++ b/test/old-code/heyting-algebras.jl @@ -1,5 +1,7 @@ -using SoleLogics +using Base using Graphs +using SoleLogics +using SoleLogics.ManyValuedLogics @test_throws AssertionError( "Cannot instantiate `HeytingAlgebra` with domain of length 0. Need to specify at " * @@ -439,7 +441,7 @@ myalgebra = HeytingAlgebra(domain, relations, evaluate=true) @test succeedeq(myalgebra, ⊤, G) == true @test succeedeq(myalgebra, ⊤, ⊤) == true -using SoleLogics: maximalmembers +using SoleLogics.ManyValuedLogics: maximalmembers @test Set{HeytingTruth}([maximalmembers(myalgebra, ⊥)...]) == Set{HeytingTruth}([HeytingTruth[]...]) @test Set{HeytingTruth}([maximalmembers(myalgebra, A)...]) == Set{HeytingTruth}([HeytingTruth[E]...]) @@ -451,7 +453,7 @@ using SoleLogics: maximalmembers @test Set{HeytingTruth}([maximalmembers(myalgebra, G)...]) == Set{HeytingTruth}([HeytingTruth[F, E]...]) @test Set{HeytingTruth}([maximalmembers(myalgebra, ⊤)...]) == Set{HeytingTruth}([HeytingTruth[F, G]...]) -using SoleLogics: minimalmembers +using SoleLogics.ManyValuedLogics: minimalmembers @test Set{HeytingTruth}([minimalmembers(myalgebra, ⊥)...]) == Set{HeytingTruth}([HeytingTruth[B, A]...]) @test Set{HeytingTruth}([minimalmembers(myalgebra, A)...]) == Set{HeytingTruth}([HeytingTruth[C, B]...]) @@ -463,7 +465,7 @@ using SoleLogics: minimalmembers @test Set{HeytingTruth}([minimalmembers(myalgebra, G)...]) == Set{HeytingTruth}([HeytingTruth[C]...]) @test Set{HeytingTruth}([minimalmembers(myalgebra, ⊤)...]) == Set{HeytingTruth}([HeytingTruth[]...]) -using SoleLogics: collatetruth +using SoleLogics.ManyValuedLogics: collatetruth @test collatetruth(∧, (⊥, ⊥), myalgebra) == HeytingTruth(⊥) @test collatetruth(∧, (⊥, A), myalgebra) == HeytingTruth(⊥) @@ -714,6 +716,7 @@ using SoleLogics: collatetruth ### Testing if check works on random propositional formulas and it gives the same result ### using Random +using SoleLogics.ManyValuedLogics: convert, @heytingtruths, @heytingalgebra booleanalgebra = @heytingalgebra () (⊥, ⊤) myalphabet = Atom.(["a", "b", "c", "d", "e", "f", "g"]) diff --git a/test/runtests.jl b/test/runtests.jl index e7d9df16..33fdb97a 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -32,12 +32,11 @@ test_suites = [ ("Kripke word", ["kripke-word.jl",]), ("Kripke image", ["kripke-image.jl",]), - ("Type Hierarchy Update", ["type-hierarchy-update.jl"]), - ("Pluto Demo", ["$(dirname(dirname(pathof(SoleLogics))))/pluto-demo.jl", ]), - ("Fuzzy", ["fuzzy.jl",]), - ("Miscellaneous", ["misc.jl",]), + ("ManyValuedLogics", ["many-valued-logics.jl",]), + + ("Miscellaneous", ["misc.jl", "util.jl"]), ] @testset "SoleLogics.jl" begin diff --git a/test/type-hierarchy-update.jl b/test/type-hierarchy-update.jl deleted file mode 100644 index ef76916d..00000000 --- a/test/type-hierarchy-update.jl +++ /dev/null @@ -1,141 +0,0 @@ -using Test -using SoleLogics - -const SL = SoleLogics # SL.name to reference unexported names - -# The following test set is intended to test the new type hierarchy update, -# considering both trivial and complex assertions regarding various aspects of SoleLogics. - -############################################################################################ -#### Declaration section ################################################################### -############################################################################################ - -p = Atom("p") -q = Atom("q") -r = Atom("r") -m = Atom(1) -n = Atom(2) - -pandq = SyntaxTree(CONJUNCTION, (p,q)) -pandq_demorgan = DISJUNCTION(p |> NEGATION, q |> NEGATION) |> NEGATION -qandp = SyntaxTree(CONJUNCTION, (q,p)) -pandr = SyntaxTree(CONJUNCTION, (p,r)) -porq = SyntaxTree(DISJUNCTION, (p,q)) -norm = SyntaxTree(DISJUNCTION, (m,n)) -trees_implication = SyntaxTree(IMPLICATION, (pandq, porq)) - -interp1 = TruthDict([p => TOP, q => TOP]) -interp2 = TruthDict(1:4, BOT) - -############################################################################################ -#### Test section ########################################################################## -############################################################################################ - -@test Formula <: Syntactical -@test AbstractSyntaxStructure <: Formula -@test SyntaxLeaf <: AbstractSyntaxStructure -@test Truth <: SyntaxLeaf - -@test TOP isa Truth -@test TOP isa BooleanTruth -@test BOT isa Truth -@test BOT isa BooleanTruth - -@test Connective <: Syntactical -@test NamedConnective <: Connective - -@test Connective <: Operator -@test Truth <: Operator -@test Connective <: SyntaxToken -@test SyntaxLeaf <: SyntaxToken - -@test SyntaxTree <: AbstractSyntaxStructure -@test SyntaxBranch <: SyntaxTree - -@test NEGATION isa NamedConnective -@test CONJUNCTION isa NamedConnective -@test DISJUNCTION isa NamedConnective -@test IMPLICATION isa NamedConnective -@test typeof(¬) <: NamedConnective -@test typeof(∧) <: NamedConnective -@test typeof(∨) <: NamedConnective -@test typeof(→) <: NamedConnective - -@test isnullary(p) == true -@test syntaxstring(p) == "p" - -@test pandq |> syntaxstring == CONJUNCTION(p, q) |> syntaxstring -@test pandq |> syntaxstring == (@synexpr p ∧ q) |> syntaxstring -@test porq |> syntaxstring == DISJUNCTION(p, q) |> syntaxstring -@test porq |> syntaxstring == (@synexpr p ∨ q) |> syntaxstring -@test trees_implication |> syntaxstring == IMPLICATION(pandq, porq) |> syntaxstring -@test trees_implication |> syntaxstring == (@synexpr pandq → porq) |> syntaxstring - -@test pandq |> syntaxstring == - SL.composeformulas(CONJUNCTION, (p, q)) |> syntaxstring -@test porq |> syntaxstring == - SL.composeformulas(DISJUNCTION, (p, q)) |> syntaxstring -@test trees_implication |> syntaxstring == - SL.composeformulas(IMPLICATION, (pandq, porq)) |> syntaxstring - -@test parseformula("p → q ∧ r") == (@synexpr p → q ∧ r) -@test parseformula("p → (q → r)") == (@synexpr p → (q → r)) -@test parseformula("p → (q ∧ r)") == (@synexpr p → (q ∧ r)) - -@test istop(@synexpr ⊤) -@test @synexpr ⊤ == TOP -@test isbot(@synexpr ⊥) -@test @synexpr ⊥ == ⊥ -@test @synexpr ⊤ ∧ ⊥ == SyntaxBranch(∧, ⊤, ⊥) -@test @synexpr ⊤ ∧ ⊥ == parseformula("⊤ ∧ ⊥") -@test @synexpr ¬⊤ == SyntaxBranch(¬, ⊤) -@test @synexpr ¬⊤ == parseformula("¬⊤") - -@test all(t -> t isa BooleanTruth, truths(@synexpr ¬⊤ → ⊥ ∨ ⊤)) - -@test normalize(@synexpr ¬⊤ → ⊥) == ⊤ -@test normalize(@synexpr ¬⊥ → ⊥) == ⊥ -@test normalize(@synexpr ⊤ ∧ ¬ ⊤) == ⊥ -@test normalize(@synexpr ⊤∧¬⊤) == ⊥ - -@test syntaxstring((@synexpr □(□(□(p))) ∧ q)) == syntaxstring(parseformula("□□□p ∧ q")) -@test syntaxstring((@synexpr □(p) ∧ q)) == syntaxstring(parseformula("□p ∧ q")) - -@test syntaxstring((@synexpr p ∧ □(□(□(q))))) == syntaxstring(parseformula("p ∧ □□□q")) -@test syntaxstring((@synexpr p ∧ □(q))) == syntaxstring(parseformula("p ∧ □q")) - -@test syntaxstring((@synexpr □(□(□(p))) → q)) == syntaxstring(parseformula("□□□p → q")) -@test syntaxstring((@synexpr □(p) → q)) == syntaxstring(parseformula("□p → q")) - -@test syntaxstring((@synexpr p → □(□(□(q))))) == syntaxstring(parseformula("p → □□□q")) -@test syntaxstring((@synexpr p → □(q))) == syntaxstring(parseformula("p → □q")) - -@test natoms(pandq) == 2 -@test natoms(trees_implication) == natoms(pandq) + natoms(porq) -@test Set(atoms(pandq)) == Set(atoms(qandp)) -@test Set(atoms(pandq)) == Set(atoms(porq)) -@test Set(atoms(pandq)) != Set(atoms(pandr)) -@test height(trees_implication) == height(pandq) + height(qandp) - -@test isequal(p, p) == true -@test isequal(p, q) == false -@test isequal(pandq, porq) == false -@test isequal(porq, porq) == true -@test isequal(pandq, pandq_demorgan) == false # This is not semantics, but syntax only. - -@test token(pandq) == CONJUNCTION -@test token(norm) == DISJUNCTION -@test token(pandq_demorgan) == NEGATION -@test token(trees_implication) == IMPLICATION - -@test trees_implication |> children |> first == pandq -@test trees_implication |> children |> last == porq - -@test norm |> children |> first == SyntaxTree(m) -@test norm |> children |> first |> token == m -@test norm |> children |> first |> token |> value == value(m) - -@test_nowarn interp1[p] = BOT -@test_nowarn interp1[p] = TOP - -@test check(pandq, interp1) == true diff --git a/test/util.jl b/test/util.jl new file mode 100644 index 00000000..9b6e26c5 --- /dev/null +++ b/test/util.jl @@ -0,0 +1,14 @@ +using SoleLogics +using Test + +@test_nowarn SoleLogics.displaysyntaxvector([Atom(1)]) +# Atom{Int64}["1"] + +@test_nowarn SoleLogics.displaysyntaxvector([Atom(1)]; quotes = false) +# Atom{Int64}[1] + +@test_nowarn SoleLogics.displaysyntaxvector(Atom.(1:20); quotes = false) +# Atom{Int64}[1, 2, 3, 4, ..., 16, 17, 18, 19, 20] + +@test_nowarn SoleLogics.displaysyntaxvector(Atom.(1:20)) +# Atom{Int64}["1", "2", "3", "4", ..., "16", "17", "18", "19", "20"]