Logic
import it.grypho.scala.leonardo.core.*
import it.grypho.scala.leonardo.logic.*
import it.grypho.scala.leonardo.parser.Parser
val a = _Variable("a")
val b = _Variable("b")
val env = new Environment()
Connectives
The logic package provides the five connectives — And, Or, Not, Implies, Xor — as ordinary expression nodes over the shared AST. Operands are untyped _Expressions, so equations and any other domain compose freely. eval runs the Kleene/Zadeh min–max rule table (and = min, or = max, not = 1 − a) and reduces to a _Bool when the operands do:
And(_Bool(true), _Bool(false)).eval(env)
// res0: Either[_Expression, _Value] = Right(value = _Bool(b = false))
In the grammar the connectives are the word operators and, or, not, implies, xor, with true/false as literals. They bind looser than =/==, with precedence (tightest to loosest) not > and > xor > or > implies (implies is right-associative):
Parser.parse("a or b and c").get
// res1: _Expression = Or(
// a = _Variable(variable = "a"),
// b = And(a = _Variable(variable = "b"), b = _Variable(variable = "c"))
// )
Parser.parse("x = 1 and y = 2").get
// res2: _Expression = And(
// a = _Equation(lhs = _Variable(variable = "x"), rhs = _Number(d = 1.0)),
// b = _Equation(lhs = _Variable(variable = "y"), rhs = _Number(d = 2.0))
// )
Parser.parse("true and false").get.eval(env)
// res3: Either[_Expression, _Value] = Right(value = _Bool(b = false))
A connective over an unbound variable stays symbolic with the operands reduced, following the library-wide dual-evaluation contract:
And(a, _Bool(true)).eval(env)
// res4: Either[_Expression, _Value] = Left(
// value = And(a = _Variable(variable = "a"), b = _Bool(b = true))
// )
And(a, _Bool(true)).eval(env.withBinding("a", _Bool(true)))
// res5: Either[_Expression, _Value] = Right(value = _Bool(b = true))
And, Or, and Implies short-circuit exactly as Product.eval does on a zero operand: false and X is false — and true or X is true — without evaluating X, even when X could not reduce at all:
// 1/0 = 0 cannot reduce, but the left operand decides
And(_Bool(false), Parser.parse("1/0 = 0").get).eval(env)
// res6: Either[_Expression, _Value] = Right(value = _Bool(b = false))
Three-valued (Kleene) logic
The same connectives and the same rule table carry a third truth value, unknown — the value carrier widens, the operators do not. unknown is _Truth.Unknown, a first-class value (bindable, printable, saved by :save) sitting at degree 0.5:
Parser.parse("unknown").get
// res7: _Expression = _Truth(d = 0.5)
Not(_Truth.Unknown).eval(env) // 0.5 is the negation fixpoint
// res8: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
And(_Truth.Unknown, _Truth.Unknown).eval(env)
// res9: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
The crisp cases still decide, because 0 annihilates min and 1 annihilates max — which is exactly why And/Or’s short-circuits stay valid unchanged:
And(_Bool(false), _Truth.Unknown).eval(env) // false and unknown = false
// res10: Either[_Expression, _Value] = Right(value = _Bool(b = false))
Or(_Bool(true), _Truth.Unknown).eval(env) // true or unknown = true
// res11: Either[_Expression, _Value] = Right(value = _Bool(b = true))
And(_Bool(true), _Truth.Unknown).eval(env) // true and unknown = unknown
// res12: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
_Truth.of collapses the crisp endpoints back to _Bool, so every boolean pattern match keeps firing and the classical truth tables come out of the graded table unchanged — the boolean logic above is a special case, not a separate path:
_Truth.of(1.0)
// res13: _Value = _Bool(b = true)
_Truth.of(0.0)
// res14: _Value = _Bool(b = false)
And(_Bool(true), _Bool(true)).eval(env) // a _Bool, not a _Truth
// res15: Either[_Expression, _Value] = Right(value = _Bool(b = true))
kleeneTable is the three-valued counterpart of truthTable, enumerating 3^n rows (up to 10 variables); the REPL spells it truth3:
kleeneTable(Not(a), List(a)).map((row, result) => (row("a").toString, result.map(_.toString)))
// res16: Vector[Tuple2[String, Option[String]]] = Vector(
// ("false", Some(value = "true")),
// ("unknown", Some(value = "unknown")),
// ("true", Some(value = "false"))
// )
leonardo> truth3 a and not a
a | (a and (not a))
false | false
unknown | unknown
true | false
That last row is the point: unknown and not unknown is unknown, not false. The classical laws that fail here — complement in and/or, a implies a, and a xor a — are gated on the expression being free of _Truth degrees, so simplification never “proves” them away:
simplifyLogicFully(And(_Truth.Unknown, Not(_Truth.Unknown))) // stays unknown
// res17: _Expression = _Truth(d = 0.5)
simplifyLogicFully(And(a, Not(a))) // free variables: crisp atoms
// res18: _Expression = _Bool(b = false)
A free variable counts as a crisp atom — that is the documented domain restriction of simplifyLogic, toCNF, and toDNF. If a variable may hold unknown, bind it and use eval rather than simplify.
Symmetric ternary: the same logic in different digits
Symmetric ternary spells the three truth values with the digits {-1, 0, 1} — the alphabet of balanced ternary — instead of {false, unknown, true}. The two alphabets are related by the affine map t = (s + 1) / 2, so this is an encoding, not a second semantics — the rule table above is untouched:
_Truth.fromSymmetric(-1.0)
// res19: _Value = _Bool(b = false)
_Truth.fromSymmetric(0.0)
// res20: _Value = _Truth(d = 0.5)
_Truth.fromSymmetric(1.0)
// res21: _Value = _Bool(b = true)
_Truth.toSymmetric(_Truth.Unknown)
// res22: Option[Double] = Some(value = 0.0)
The encoding is switched on per Environment (the REPL spells it logic symmetric on). With it on, the digits are additionally read as truth values in connective positions, and the Kleene identities restate verbatim:
val sym = new Environment(Environment.DefaultPrecision, Map.empty, symmetricLogic = true)
Parser.parse("-1 and 0").get.eval(sym) // false and unknown = false
// res23: Either[_Expression, _Value] = Right(value = _Bool(b = false))
Parser.parse("1 or 0").get.eval(sym) // true or unknown = true
// res24: Either[_Expression, _Value] = Right(value = _Bool(b = true))
Parser.parse("0 and 0").get.eval(sym) // unknown and unknown = unknown
// res25: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
Parser.parse("not 0").get.eval(sym) // not unknown = unknown
// res26: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
The guard matters: with the encoding off a bare 0 is a plain number, so a connective over it stays symbolic rather than silently becoming a truth value, and ordinary arithmetic is never reinterpreted in either mode:
And(_Number(1.0), _Number(0.0)).eval(env) // default: stays symbolic
// res27: Either[_Expression, _Value] = Left(
// value = And(a = _Number(d = 1.0), b = _Number(d = 0.0))
// )
Parser.parse("2 * 3 + 1").get.eval(sym) // symmetric: still just arithmetic
// res28: Either[_Expression, _Value] = Right(value = _Number(d = 7.0))
Because the flag lives on the Environment, a bound variable participates too — which a purely textual encoding could not do:
And(a, _Bool(true)).eval(sym.withBinding("a", _Number(0.0)))
// res29: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
One consequence worth noting: under this encoding the digit 0 is unknown, so it counts as graded for the crisp-only gate — 0 and not 0 must not fold to false by complement:
simplifyLogicFully(And(_Number(0.0), Not(_Number(0.0))), identity, symmetric = true)
// res30: _Expression = _Truth(d = 0.5)
At the REPL the toggle is persisted by :save, but the script always writes the word spelling, so saved sessions stay portable across the setting:
leonardo> logic symmetric on
leonardo> truth3 not a
a | (not a)
-1 | 1
0 | 0
1 | -1
Fuzzy logic: the full [0, 1] interval
The _Truth carrier already holds any degree in [0, 1], so the fuzzy tier needs no new value type — only a way to produce degrees and a choice of how they combine. truth(x) converts a scalar degree, and is also how a graded degree prints, so it round-trips:
Parser.parse("truth(0.25)").get.eval(env)
// res31: Either[_Expression, _Value] = Right(value = _Truth(d = 0.25))
_Truth.of(0.25).toString
// res32: String = "truth(0.25)"
And(_Truth.of(0.3), _Truth.of(0.7)).eval(env) // min
// res33: Either[_Expression, _Value] = Right(value = _Truth(d = 0.3))
Not(_Truth.of(0.3)).eval(env) // 1 - a
// res34: Either[_Expression, _Value] = Right(value = _Truth(d = 0.7))
Membership functions and hedges
Membership curves map a crisp measurement into [0, 1], and the hedges reshape a degree. They evaluate to truth values, so they compose with the connectives directly — no cast at each step:
Parser.parse("trimf(2.5, 0, 5, 10)").get.eval(env) // triangular, halfway up
// res35: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
Parser.parse("gaussmf(3, 3, 1)").get.eval(env) // gaussian, at the mean
// res36: Either[_Expression, _Value] = Right(value = _Bool(b = true))
Parser.parse("very(0.5)").get.eval(env) // concentration: d squared
// res37: Either[_Expression, _Value] = Right(value = _Truth(d = 0.25))
Parser.parse("somewhat(0.25)").get.eval(env) // dilation: sqrt d
// res38: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
Parser.parse("very(0.5) and somewhat(0.25)").get.eval(env)
// res39: Either[_Expression, _Value] = Right(value = _Truth(d = 0.25))
The built-in set is trimf(x, a, b, c), trapmf(x, a, b, c, d), gaussmf(x, mean, sigma), sigmf(x, a, c), plus the hedges very and somewhat.
Custom membership functions
The built-in curves are a convenience, not a limit: truth(x) takes an arbitrary scalar expression, so any function of one variable is a membership curve. Here is a Cauchy bell, which is none of the four built-in shapes:
val bell = Parser.parse("truth(1 / (1 + (x - 5)^2))").get
def at(v: Double) = bell.eval(env.withBinding("x", _Number(v)))
at(5.0) // the centre
// res40: Either[_Expression, _Value] = Right(value = _Bool(b = true))
at(4.0) // one unit out
// res41: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
at(0.0)
// res42: Either[_Expression, _Value] = Right(
// value = _Truth(d = 0.038461538461538464)
// )
A custom curve is not second-class — it composes with the hedges, the connectives and defuzz exactly like a built-in one:
Parser.parse("very(truth(1 / (1 + (x - 5)^2)))").get.eval(env.withBinding("x", _Number(4.0)))
// res43: Either[_Expression, _Value] = Right(value = _Truth(d = 0.25))
centroid(bell, _Variable("x"), 0.0, 10.0)
// res44: Option[Double] = Some(value = 5.000000000000004)
At the REPL a curve is usually given a name first, and then used by that name:
leonardo> bell := truth(1 / (1 + (x - 5)^2))
leonardo> defuzz(bell, x, 0, 10)
5.0
Two rules worth knowing. First, a membership degree lives in [0, 1]: an argument outside that interval is not a degree, so the node stays symbolic rather than clamping — which is how a custom curve tells you it has left the unit interval.
Parser.parse("truth(2)").get.eval(env) // stays symbolic, not clamped to true
// res45: Either[_Expression, _Value] = Left(
// value = _TruthOf(a = _Number(d = 2.0))
// )
Second, defuzz also accepts a bare scalar curve with no truth(...) wrapper, and either way only points inside [0, 1] count as membership:
Parser.parse("defuzz(1 / (1 + (x - 5)^2), x, 0, 10)").get.eval(env)
// res46: Either[_Expression, _Value] = Right(
// value = _Number(d = 5.000000000000004)
// )
Aggregating curves
Because degrees are truth values, curves combine with the ordinary connectives — the usual fuzzy-inference step, where each rule contributes a curve and the results are unioned before defuzzifying:
Parser.parse("defuzz(trimf(x, 0, 3, 6) or trimf(x, 4, 7, 10), x, 0, 10)").get.eval(env)
// res47: Either[_Expression, _Value] = Right(
// value = _Number(d = 4.999999999999999)
// )
The connectives are admitted in the membership positions specifically — the argument of defuzz, very, and somewhat. Ordinary function arguments stay arithmetic, so sin(a and b) is still a parse error.
Alternative t-norms
Which t-norm combines degrees is an Environment parameter, not a separate package or node: min–max (the default), product, or Łukasiewicz. All three agree with classical logic on the crisp values, so the boolean and three-valued tiers are unaffected:
val prod = new Environment(Environment.DefaultPrecision, Map.empty, false, LogicSemantics.Product)
val lukas = new Environment(Environment.DefaultPrecision, Map.empty, false, LogicSemantics.Lukasiewicz)
And(_Truth.of(0.3), _Truth.of(0.5)).eval(prod) // 0.3 * 0.5
// res48: Either[_Expression, _Value] = Right(value = _Truth(d = 0.15))
Or(_Truth.of(0.3), _Truth.of(0.5)).eval(prod) // a + b - a*b
// res49: Either[_Expression, _Value] = Right(value = _Truth(d = 0.65))
And(_Truth.of(0.8), _Truth.of(0.7)).eval(lukas) // max(0, 1.5 - 1)
// res50: Either[_Expression, _Value] = Right(value = _Truth(d = 0.5))
And(_Bool(true), _Bool(true)).eval(lukas) // crisp: unchanged
// res51: Either[_Expression, _Value] = Right(value = _Bool(b = true))
Only min–max is a lattice, so idempotence and absorption hold for graded degrees there alone — a and a is a squared under the product t-norm. Simplification gates those two rules on the semantics accordingly, on top of the crisp-only gate above:
simplifyLogicFully(And(_Truth.of(0.3), _Truth.of(0.3)), identity, false, LogicSemantics.MinMax)
// res52: _Expression = _Truth(d = 0.3)
simplifyLogicFully(And(_Truth.of(0.3), _Truth.of(0.3)), identity, false, LogicSemantics.Product)
// res53: _Expression = _Truth(d = 0.09)
Defuzzification
Defuzzifying collapses a membership curve back to one crisp value. centroid (the centre of gravity) is what defuzz(e, v, lo, hi) uses in the grammar; meanOfMaxima and bisector are available as library functions:
val tri = Parser.parse("trimf(x, 0, 5, 10)").get
// tri: _Expression = TriMF(
// x = _Variable(variable = "x"),
// a = _Number(d = 0.0),
// b = _Number(d = 5.0),
// c = _Number(d = 10.0)
// )
centroid(tri, _Variable("x"), 0.0, 10.0)
// res54: Option[Double] = Some(value = 4.999999999999998)
meanOfMaxima(tri, _Variable("x"), 0.0, 10.0)
// res55: Option[Double] = Some(value = 5.0)
Parser.parse("defuzz(trimf(x, 0, 5, 10), x, 0, 10)").get.eval(env)
// res56: Either[_Expression, _Value] = Right(
// value = _Number(d = 4.999999999999998)
// )
Sampling takes scalar.compile’s fast path when the curve is pure scalar arithmetic and falls back to tree evaluation for membership and connective nodes — this is where logic gains its scalar import, the same relationship matrix already has.
Simplification
simplifyLogic (and its fixpoint simplifyLogicFully) applies constant folding, double negation, idempotence, complement, and absorption:
simplifyLogicFully(And(a, _Bool(true)))
// res57: _Expression = _Variable(variable = "a")
simplifyLogicFully(Not(Not(a)))
// res58: _Expression = _Variable(variable = "a")
simplifyLogicFully(Or(a, And(a, b)))
// res59: _Expression = _Variable(variable = "a")
simplifyLogicFully(And(a, Not(a)))
// res60: _Expression = _Bool(b = false)
The REPL’s simplify command runs this pass after the scalar pass, injecting scalar.simplifyFully for scalar bodies nested inside connectives.
Normal forms
toCNF / toDNF rewrite an expression into conjunctive / disjunctive normal form: implies/xor are desugared, not is pushed to the leaves via De Morgan’s laws, and the appropriate connective is distributed. A distribution that would exceed 1024 clauses returns the input unchanged:
toCNF(Not(And(a, b)))
// res61: _Expression = Or(
// a = Not(a = _Variable(variable = "a")),
// b = Not(a = _Variable(variable = "b"))
// )
toCNF(Implies(a, b))
// res62: _Expression = Or(
// a = Not(a = _Variable(variable = "a")),
// b = _Variable(variable = "b")
// )
toDNF(And(a, Or(b, _Variable("c"))))
// res63: _Expression = Or(
// a = And(a = _Variable(variable = "a"), b = _Variable(variable = "b")),
// b = And(a = _Variable(variable = "a"), b = _Variable(variable = "c"))
// )
toCNF(Or(a, Not(a)))
// res64: _Expression = _Bool(b = true)
These algorithms are crisp-only: they treat non-connective sub-expressions as opaque atoms and are valid for boolean operands only.
Truth tables
truthTable enumerates every boolean assignment of a variable list (up to 16 variables) and evaluates the expression under each; rows that cannot reduce to a boolean yield None:
truthTable(Xor(a, b), List(a, b))
// res65: Vector[Tuple2[Map[String, Boolean], Option[Boolean]]] = Vector(
// (Map("a" -> false, "b" -> false), Some(value = false)),
// (Map("a" -> false, "b" -> true), Some(value = true)),
// (Map("a" -> true, "b" -> false), Some(value = true)),
// (Map("a" -> true, "b" -> true), Some(value = false))
// )
The REPL command truth <expr> prints the same table over the expression’s free variables:
leonardo> truth a and b
a b | (a and b)
false false | false
false true | false
true false | false
true true | true