Similarity-based OSF logic

The language of OSF logic is extended with a similarity relation on sort symbols.

from fosf.parsers import parse_taxonomy
taxonomy_decs = """
# sort subsumption
person, string, movie < top .

historical, fantasy, horror, thriller < movie .
scifi < fantasy .
psych_horror < horror .
psych_thriller < thriller .

director, producer, writer < person .
thrillerdirector < director.
horrorwriter < writer.

# sort similarity
psych_thriller ~ psych_horror = 0.5 .
historical ~ fantasy = 0.2 .
"""
tax = parse_taxonomy(taxonomy_decs)

The subsumption and similarity relations are combined into a single fuzzy subsumption relation. E.g., since

• psych_thriller ~ psych_horror = 0.5 , and

• psych_horror < horror, then

• psych_thriller < horror with degree $0.5$.

We can visualize the resulting fuzzy taxonomy (and the background similarity).

from fosf.utils.draw import notebook_display as display
display(tax, similarity=tax._similarity)

from fosf.syntax import Sort
movie = Sort('movie')
horror = Sort('horror')
thriller = Sort('thriller')
psych_horror = Sort('psych_horror')
psych_thriller = Sort('psych_thriller')
historical = Sort('historical')
fantasy = Sort('fantasy')
scifi = Sort('scifi')

We can thus compute GLBs:

tax.glb(historical, fantasy)

Sort('scifi')

And also subsumption degrees:

tax.degree(scifi, historical)

np.float64(0.2)

tax.degree(psych_horror, movie)

1.0

Since horror and thriller don’t have a GLB, we obtain maximal lower bounds (MLBs) instead, which are treated as a disjunctive set of sorts.

tax.glb(horror, thriller)

FrozenDisjunctiveSort(Sort('psych_horror'), Sort('psych_thriller'))

psych_thriller and psych_horror don’t have a GLB or MLBs, but they are similar, so we also obtain a disjunctive set of sorts:

tax.glb(psych_thriller, psych_horror)

FrozenDisjunctiveSort(Sort('psych_horror'), Sort('psych_thriller'))

Disjunctive sorts are printed inside curly braces:

print(tax.glb(psych_thriller, psych_horror))

{ psych_horror, psych_thriller }

Similarity-based OSF term normalization

The similarity relation is taken into account when normalizing or unifying OSF terms.

from fosf.parsers import parse_term
term1_str = "X0:psych_horror(directed_by -> X1)"
term2_str = "Y0:psych_thriller(directed_by -> Y1, written_by -> Y1:writer)"
term1, term2 = parse_term(term1_str), parse_term(term2_str)
print("Term 1 to be unified:")
term1.pretty_print()
print("\nTerm 2 to be unified:")
term2.pretty_print()

Term 1 to be unified:
X0 : psych_horror(
    directed_by -> X1
)


Term 2 to be unified:
Y0 : psych_thriller(
    directed_by -> Y1
    written_by -> Y1 : writer
)

from fosf.reasoning import unify_terms
unif, degree = unify_terms([term1, term2], tax, return_degree=True)
print("Unifier:\n"+unif.prettify() + f"with unification degree: {degree}")

Unifier:
X0 : { psych_horror, psych_thriller }(
    directed_by -> X1 : writer
    written_by -> X1
)
with unification degree: 0.5

from fosf.utils.draw import unification_to_agraph
display(unification_to_agraph([term1, term2], tax))

Similarity-based OSF term normalization modulo an OSF theory

Defining an OSF theory:

from fosf.parsers import parse_theory
theory_str = taxonomy_decs + """
    # sort definitions
    
    person := Yp:person(spouse -> Y1:person(spouse    -> Yp,
                                            last_name -> Yn:string),
                        last_name -> Yn).
                        
    thrillerdirector := Yt:thrillerdirector(director_of -> Y2: thriller).
    
    horrorwriter := Yh:horrorwriter(writer_of -> Y3: horror).
    
    movie  := Ym:movie(directed_by -> Y5: director(director_of -> Ym),
                       written_by  -> Y6: writer(writer_of -> Ym)).


    # feature domain & ranges
    
    domain(director_of) := director . range(director_of) := movie .
    domain(directed_by) := movie .    range(directed_by) := director .
    domain(writer_of)   := writer .   range(writer_of)   := movie .
    domain(written_by)  := movie .    range(written_by)  := writer .
"""

theory = parse_theory(theory_str, ensure_closed=True)

Term to normalize modulo the OSF theory:

term_str = """
X(directed_by -> X0:thrillerdirector(spouse -> X1),
  written_by  -> X1:horrorwriter(spouse -> X0) )
"""
term = parse_term(term_str)
display(term)

Because X must be a thriller and also a horror according to the theory, then it must be of sort glb(thriller, horror):

tax.glb(thriller, horror)

FrozenDisjunctiveSort(Sort('psych_horror'), Sort('psych_thriller'))

Theory normalization will take this disjunction into account, and return a disjunctive term:

from fosf.reasoning import normalize_term
normal_term, alpha = normalize_term(term, theory.taxonomy, theory, return_degree=True)
print(normal_term.prettify() + f"Satisfaction degree: {alpha}")

T0 : {
    X : psych_horror(
        directed_by -> X0 : thrillerdirector(
            spouse -> X1 : horrorwriter(
                spouse -> X0
                writer_of -> X
            )
            director_of -> X
        )
        written_by -> X1
    )
    ;
    X : psych_thriller(
        directed_by -> X0 : thrillerdirector(
            spouse -> X1 : horrorwriter(
                spouse -> X0
                writer_of -> X
            )
            director_of -> X
        )
        written_by -> X1
    )
}
Satisfaction degree: 0.5

Translating this term to SPARQL yields a union:

print(normal_term.to_sparql())

prefix : <http://example.org/>
SELECT DISTINCT ?T0 WHERE {
  {
    ?X rdf:type :psych_horror .
    ?X :directed_by ?X0 .
    ?X0 rdf:type :thrillerdirector .
    ?X0 :spouse ?X1 .
    ?X1 rdf:type :horrorwriter .
    ?X1 :spouse ?X0 .
    ?X1 :writer_of ?X .
    ?X0 :director_of ?X .
    ?X :written_by ?X1 .
    BIND(?X AS ?T0)
  }
  UNION
  {
    ?X rdf:type :psych_thriller .
    ?X :directed_by ?X0 .
    ?X0 rdf:type :thrillerdirector .
    ?X0 :spouse ?X1 .
    ?X1 rdf:type :horrorwriter .
    ?X1 :spouse ?X0 .
    ?X1 :writer_of ?X .
    ?X0 :director_of ?X .
    ?X :written_by ?X1 .
    BIND(?X AS ?T0)
  }
}

However, since the two disjunct share a majority of constriants, the term can be simplified:

from fosf.utils.terms import simplify_disjunctive_term
simplified = simplify_disjunctive_term(normal_term)
simplified.pretty_print()

X : { psych_horror, psych_thriller }(
    directed_by -> X0 : thrillerdirector(
        director_of -> X
        spouse -> X1 : horrorwriter(
            spouse -> X0
            writer_of -> X
        )
    )
    written_by -> X1
)

display(simplified)

The SPARQL translation of the term will take the disjunction into account:

print(simplified.to_sparql())

prefix : <http://example.org/>
SELECT DISTINCT ?X WHERE {
  ?X rdf:type ?type0 .
  VALUES ?type0 { :psych_horror :psych_thriller }
  ?X :directed_by ?X0 .
  ?X0 rdf:type :thrillerdirector .
  ?X0 :director_of ?X .
  ?X0 :spouse ?X1 .
  ?X1 rdf:type :horrorwriter .
  ?X1 :spouse ?X0 .
  ?X1 :writer_of ?X .
  ?X :written_by ?X1 .
}