relative-meta-logic

A prototype for logic framework that can reason about anything relative to given probability of input statements.

Note on naming: This project was previously called Associative-Dependent Logic (ADL). The name Associative Dependent Meta Logic is also valid, as in dependent types, but relative is closer to the concept of a link, and actually all statements are relative to other statements. The name meta-logic reflects that this system can reason about all possible logic systems, including itself.

Implementations

This project provides two equivalent implementations:

• JavaScript — Node.js implementation using the official links-notation parser
• Rust — Rust implementation using the official links-notation crate

Both implementations pass the same comprehensive test suites and produce identical results.

For implementation details, see ARCHITECTURE.md.

Comparisons

• Core concept comparison - RML vs Twelf, LF, HELF, Isabelle, Coq/Rocq, Lean, Foundation, AFP, Abella, lambda Prolog, and Pecan by logical/metatheoretic concepts.
• Product feature comparison - RML vs the same systems by authoring workflow, automation, libraries, tooling, and distribution.
• Configurability and operator redefinition - Why every operator, truth constant, range, and valence is redefinable at runtime, with the precedence rules and a comparison to Lean/Rocq fixed semantics.
• Typed kernel rules - The implemented D1 rules for Pi, lambda, apply, (expr of Type), and (type of expr).
• Soundness statement - The trusted-kernel guarantee, proof-replay checker, trusted operator base, and aggregator-relative scope of soundness.
• Metatheorem checker - The C3 Twelf-style guarantee that composes D12 totality, D14 coverage, D15 modes, and D13 termination, plus the rml-meta CLI.
• Lean 4 export - The rml export lean bridge for typed, non-probabilistic RML fragments.
• Rocq export - The supported typed LiNo subset for rml export rocq <file.lino> -o <file.v>.

Overview

RML (Relative Meta-Logic, formerly Associative-Dependent Logic / ADL) is a minimal probabilistic logic system built on top of LiNo (Links Notation). It supports many-valued logics from unary (1-valued) through continuous probabilistic (fuzzy), allowing you to:

• Define terms
• Assign probabilities (truth values) to logical expressions
• Redefine logical operators with different semantics
• Configure truth value ranges: [0, 1] or [-1, 1] (balanced/symmetric)
• Configure logic valence: 2-valued (Boolean), 3-valued (ternary/Kleene), N-valued, or continuous
• Use and redefine truth constants: true, false, unknown, undefined
• Use and redefine Belnap operators: both...and (contradiction/avg) and neither...nor (gap/product)
• Resolve paradoxical statements (e.g. the liar paradox)
• Perform decimal-precision arithmetic (+, -, *, /) — 0.1 + 0.2 = 0.3, not 0.30000000000000004
• Query the truth value of complex expressions
• Define dependent types as links — universe hierarchy, Pi-types, lambdas, type queries
• Combine types with probabilistic logic in a unified framework
• Delegate domain-specific decision blocks through evaluator plugins, including (domain automatic-sequences (theorem thue-morse-cube-free))
• Reuse the evaluator as a library, including a meta-expression adapter that accepts selected interpretations and explicit dependencies while keeping underspecified claims partial
• Export the simply typed LiNo fragment to Isabelle/HOL source for external certification experiments

Supported Logic Types

Valence	Name	Truth Values (in [0, 1])	Truth Values (in [-1, 1])	Reference
1	Unary (trivial)	{any} (no quantization)	{any} (no quantization)	Many-valued logic
2	Binary / Boolean	{0, 1} (false, true)	{-1, 1} (false, true)	Classical logic
3	Ternary / Three-valued	{0, 0.5, 1} (false, unknown, true)	{-1, 0, 1} (false, unknown, true)	Kleene logic, Łukasiewicz logic, Balanced ternary
4	Quaternary	{0, ⅓, ⅔, 1}	{-1, -⅓, ⅓, 1}	Belnap's four-valued logic
5	Quinary	{0, 0.25, 0.5, 0.75, 1}	{-1, -0.5, 0, 0.5, 1}	Many-valued logic
N	N-valued	N evenly-spaced levels	N evenly-spaced levels	Many-valued logic
0/∞	Continuous / Fuzzy	Any value in [0, 1]	Any value in [-1, 1]	Fuzzy logic, Łukasiewicz ∞-valued

Quick Start

JavaScript

cd js
npm install
node src/rml-links.mjs ../examples/demo.lino
node src/rml-links.mjs export lean ../examples/lean-export-basic.lino -o out.lean

Rust

cd rust
cargo run -- ../examples/demo.lino
cargo run -- export lean ../examples/lean-export-basic.lino -o out.lean

Examples are language-agnostic and live in /examples/. Both implementations execute the same files and are required to produce identical output (enforced by examples/expected.lino and the shared-examples tests).

Standard libraries

Reusable LiNo libraries live under /lib/. The classical Boolean library configures two-valued truth values and exports connectives, laws, and natural-deduction rule schemas from the classical namespace:

(import "lib/classical/core.lino" as cl)
(? (cl.or p (cl.not p)))
(? (cl.excluded-middle p))

The first-order library exports aliasable quantifier templates from the first-order namespace:

(import "lib/first-order/core.lino" as fo)
(? (fo.forall (Term x) (predicate x)))
(? ((fo.exists (Term x) (predicate x)) = (exists (Term x) (predicate x))))

The higher-order library exports quantifier templates for predicate binders from the higher-order namespace:

(import "lib/higher-order/core.lino" as ho)
(? (ho.forall ((Pi (Natural n) Boolean) P)
     ((P zero) implies (ho.forall (Natural n) (P (succ n))))))

The modal library exports normal modal operators, K/T/S4/S5 axiom schemas, and Kripke-frame interpretation templates from the modal namespace:

(import "lib/modal/core.lino" as ml)
(? (ml.axiom-k p q))
(? (ml.necessarily-at current p))

The provability library exports GL axiom schemas and a basic interpretability fragment from the provability namespace:

(import "lib/provability/core.lino" as pr)
(? (pr.provability-of p))
(? (pr.axiom-gl p))
(? (pr.interprets theory-a theory-b))

The set-theory library exports membership, basic set constructors, and ZF-style axiom schemas from the set-theory namespace:

(import "lib/set-theory/core.lino" as st)
(? (st.member-of x (set-of-naturals)))
(? (st.axiom-extensionality a b))

The arithmetic library exports Peano naturals, addition/order templates, and decimal-precision lemmas from the arithmetic namespace:

(import "lib/arithmetic/core.lino" as ar)
(? ((plus zero zero) = zero))
(? (ar.less-than zero (succ zero)))
(? (ar.decimal-sum-equals 0.1 0.2 0.3))

The algebra library exports operation laws and magma, semigroup, monoid, group, abelian-group, and unital-ring schemas from the algebra namespace:

(import "lib/algebra/core.lino" as al)
(? (al.group (carrier G) (op times) (identity e) (inverse inv)))
(? (al.ring R plus zero neg times one))

The programming-language theory library exports untyped lambda-calculus constructors, simply typed lambda calculus typing and small-step schemas, and type-safety theorem forms from the programming-language namespace:

(import "lib/programming-language/core.lino" as pl)
(? (pl.theorem progress (pl.progress term T)))
(? (pl.theorem preservation (pl.preservation term next T)))

The probabilistic library packages Bayesian-network, fuzzy-control, Belnap-bilattice, and paradox-catalogue helpers as standard LiNo imports:

(import "lib/probabilistic/bayesian.lino" as bn)
(import "lib/probabilistic/fuzzy.lino" as fz)
(import "lib/probabilistic/belnap.lino" as bl)
(import "lib/probabilistic/paradoxes.lino" as px)
(bn.network sprinkler-network (nodes cloudy rain) (edges (bn.edge cloudy rain)))
(bn.prior rain 0.5)
(fz.membership temperature hot 0.8)
(fz.membership humidity wet 0.6)
(s: s is s)
(px.midpoint (px.liar s))
(? (bn.joint (rain = true) (rain = true)))
(? (fz.rule (fz.degree temperature hot) (fz.degree humidity wet)))
(? (bl.contradiction true false))
(? (px.fixed-point (px.liar s)))

Isabelle export

node js/src/rml-links.mjs export isabelle examples/isabelle-typed-fragment.lino -o Isabelle_Typed_Fragment.thy

The exporter covers the simply typed fragment documented in docs/ISABELLE-EXPORT.md.

Rocq Export

Both CLIs can translate the supported typed fragment to Rocq source:

node js/src/rml-links.mjs export rocq examples/dependent-types.lino -o dependent_types.v
cargo run --manifest-path rust/Cargo.toml -- export rocq examples/dependent-types.lino -o dependent_types.v

See docs/ROCQ-EXPORT.md for the accepted subset.

Example

Create a file example.lino:

# Classical Boolean logic
(valence: 2)
(and: min)
(or: max)

# Define propositions
(p: p is p)
(q: q is q)

# Assign truth values
((p = true) has probability 1)
((q = true) has probability 0)

# Query
(? ((p = true) and (q = true)))          # -> 0 (true AND false = false)
(? ((p = true) or (q = true)))           # -> 1 (true OR false = true)
(? ((p = true) or (not (p = true))))     # -> 1 (law of excluded middle)

Output:

0
1
1

Syntax

Term Definitions

(term_name: term_name is term_name)

Example: (a: a is a) declares a as a term.

Probability Assignments

((<expression>) has probability <value>)

Example: ((a = a) has probability 1) assigns probability 1 to the expression a = a.

Templates

(template (<name> <param>...)
  <body>)

Templates name reusable link shapes. A later use (<name> arg...) is expanded before evaluation, and template placeholders are substituted hygienically so binders introduced by the template do not capture free variables from the arguments.

(template (known expr value)
  (expr has probability value))

(known (a = b) 1)
(? (a = b))  # -> 1

Range Configuration

(range: <lo> <hi>)

Sets the truth value range. Default is [0, 1] (standard probabilistic). Use (range: -1 1) for balanced/symmetric range where the midpoint is 0.

See: Balanced ternary

Valence Configuration

(valence: <N>)

Sets the number of discrete truth values. Default is 0 (continuous, no quantization).

• (valence: 2) — Boolean logic: truth values are quantized to {0, 1}
• (valence: 3) — Ternary logic: truth values are quantized to {0, 0.5, 1}
• (valence: N) — N-valued logic: truth values are quantized to N evenly-spaced levels

Truth Constants

The symbols true, false, unknown, and undefined are predefined with values based on the current range:

Constant	Default in [0, 1]	Default in [-1, 1]	Definition	Interpretation
true	1	1	max(range)	Definitely true
false	0	-1	min(range)	Definitely false
unknown	0.5	0	mid(range)	Truth value not known
undefined	0.5	0	mid(range)	Not yet defined

These constants can be used directly in expressions:

(? true)              # -> 1 in [0,1], 1 in [-1,1]
(? false)             # -> 0 in [0,1], -1 in [-1,1]
(? unknown)           # -> 0.5 in [0,1], 0 in [-1,1]
(? (not true))        # -> 0 in [0,1], -1 in [-1,1]
(? (true and false))  # -> 0.5 (avg), 0 (avg in [-1,1])

All truth constants can be redefined to custom values:

(true: 0.8)           # Redefine true to 0.8
(false: 0.2)          # Redefine false to 0.2
(? true)              # -> 0.8
(? false)             # -> 0.2

Belnap Operators: both and neither

The operators both and neither come from Belnap's four-valued logic, where contradictions and gaps are first-class concepts. These are composite natural language operators that alter the AND operation:

Operator	Default Aggregator	Example	Result	Interpretation
both...and	avg	(both true and false)	0.5	Both true and false (contradiction)
neither...nor	product	(neither true nor false)	0	Neither true nor false (gap)

# Contradiction: both true and false
(? (both true and false))     # -> 0.5 (avg of 1 and 0)
(? (both true and true))      # -> 1   (both agree: true)

# Gap: neither true nor false
(? (neither true nor false))  # -> 0   (product of 1 and 0)
(? (neither true nor true))   # -> 1   (both agree: true)

Both operators are redefinable via aggregator selection, just like and and or:

(both: min)                   # Redefine both to use min
(? (both true and false))     # -> 0
(neither: max)                # Redefine neither to use max
(? (neither true nor false))  # -> 1

This allows paradoxes like the liar paradox to be expressed naturally:

(a: a is a)
((a = a) has probability 1)
((a != a) has probability 0)
(? (both (a = a) and (a != a)))     # -> 0.5 (contradiction resolves to midpoint)
(? (neither (a = a) nor (a != a)))  # -> 0   (gap: no info propagates)

When the range changes (via (range: ...)), all truth constants are automatically re-initialized to their defaults for the new range.

Operator Redefinitions

Binary operator composition

(operator: unary_op binary_op)

Example: (!=: not =) defines != as the negation of =.

Aggregator selection

For and and or operators, you can choose different aggregators:

(and: avg)               # Average (default)
(and: min)               # Minimum (Kleene/Łukasiewicz AND)
(and: max)               # Maximum
(and: product)           # Product (also: prod)
(and: probabilistic_sum) # Probabilistic sum: 1 - (1-p1)*(1-p2)*... (also: ps)

(or: max)                # Maximum (default, Kleene/Łukasiewicz OR)
(or: avg)                # Average
(or: min)                # Minimum
(or: product)            # Product (also: prod)
(or: probabilistic_sum)  # Probabilistic sum (also: ps)

Arithmetic

(<A> + <B>)   # Addition
(<A> - <B>)   # Subtraction
(<A> * <B>)   # Multiplication
(<A> / <B>)   # Division

All arithmetic uses decimal-precision rounding (12 significant decimal places) to eliminate IEEE-754 floating-point artefacts:

(? (0.1 + 0.2))             # -> 0.3  (not 0.30000000000000004)
(? ((0.1 + 0.2) = 0.3))     # -> 1    (true)
(? ((0.3 - 0.1) = 0.2))     # -> 1    (true)

Arithmetic operands are not clamped to the logic range, allowing natural numeric computation. Clamping occurs only when results are used in a logical context (queries, and, or, etc.).

Queries

(? <expression>)

Queries are evaluated and their truth value is printed to stdout.

Comments

# Line comments start with #
(a: a is a)  # Inline comments are also supported

Dependent Type System

Types are just links — "everything is a link". The type system coexists with probabilistic logic. ADL is a dynamic axiomatic system: every link is a recursive fractal, definitions can be changed at any time, and the system embraces self-reference and paradoxes rather than forbidding them.

Self-Referential Type: (Type: Type Type)

The primary way to define the root type in ADL is self-referential — Type is its own type:

(Type: Type Type)

This follows the pattern (SubType: Type SubType) applied to Type itself. Unlike classical type theory (Lean, Rocq) which forbids Type : Type to avoid Russell's paradox, ADL's many-valued logic resolves paradoxes to the midpoint of the truth value range (0.5 in [0,1], 0 in [-1,1]). This makes self-referential types safe and useful.

(Type: Type Type)
(Natural: Type Natural)
(Boolean: Type Boolean)
(zero: Natural zero)
(true-val: Boolean true-val)
(? (Type of Type))               # -> 1
(? (Natural of Type))            # -> 1
(? (zero of Natural))            # -> 1
(? (type of Natural))            # -> Type

Universe Hierarchy (Lean/Rocq Compatibility)

For compatibility with Lean 4 and Rocq (Coq), ADL also supports a stratified universe hierarchy where each (Type N) is a member of (Type N+1):

• (Type 0) — the universe of "small" types (Natural, Boolean, etc.)
• (Type 1) — the universe that contains (Type 0) and types formed from (Type 0) types
• (Type 2) — contains (Type 1), and so on

This mirrors Lean 4 (Type 0, Type 1, ...) and Rocq (Set, Type, ...).

Both systems can coexist — use (Type: Type Type) for the self-referential approach, and (Type N) when you need stratified universes:

(Type: Type Type)
(Type 0)
(Type 1)
(Natural: (Type 0) Natural)      # Natural in universe 0
(Boolean: Type Boolean)           # Boolean under self-referential Type
(? (Natural of (Type 0)))        # -> 1
(? (Boolean of Type))            # -> 1
(? ((Type 0) of (Type 1)))       # -> 1

Type Declarations

# Type definition follows the pattern: (SubType: Type SubType)
(Type: Type Type)
(Natural: Type Natural)
(Boolean: Type Boolean)

# Typed term via prefix type notation: (name: TypeName name)
(zero: Natural zero)
(true-val: Boolean true-val)

Pi-types (Dependent Products)

# (Pi (TypeName varName) ReturnType)
(succ: (Pi (Natural n) Natural))

Lambda Abstraction

# (lambda (TypeName varName) body)
(identity: lambda (Natural x) x)

# Multi-parameter: (lambda (TypeName x, TypeName y) body)
(add: lambda (Natural x, Natural y) (x + y))

Application

# Explicit: (apply function argument)
(? (apply identity 0.7))         # -> 0.7

# Prefix: (functionName argument)
(? (identity 0.7))               # -> 0.7

Program Extraction

Typed lambda programs that do not use probabilistic operators can be extracted to JavaScript or Rust:

rml extract js program.lino > program.mjs
rml extract rust program.lino > program.rs

Extraction erases LiNo type annotations, turns named lambda definitions into plain functions, and converts equality queries into generated tests. Programs that contain probability assignments or logical/probabilistic operators are rejected instead of being silently compiled.

Normalization

Two surface-form drivers expose the typed-fragment normalizer. whnf reduces only the outer spine; nf (alias normal-form) reduces every redex, including those nested under binders.

(Term: (Type 0) Term)
(zero: Term zero)
(succ: (Pi (Term n) Term))
(compose: lambda (Term f) (lambda (Term g) (lambda (Term x) (apply f (apply g x)))))

(? (whnf (apply (apply (apply compose succ) succ) zero)))
# -> (apply succ (apply succ zero))   # outer spine reduced, inner redex left

(? (normal-form (apply (apply (apply compose succ) succ) zero)))
# -> (succ (succ zero))               # full beta-normal form

Both are also available as library functions: whnf(term, ctx) and nf(term, ctx) in JavaScript, whnf(&term, &mut env) and nf(&term, &mut env) in Rust.

Tactic Links

The library exposes a tactic engine for composable proof-state steps while preserving the "everything is a link" invariant. Tactics are ordinary links, and successful tactic history is stored as links in the proof state:

(by reflexivity)
(symmetry)
(transitivity b)
(suppose (p = q))
(introduce n)
(rewrite (a = b) in goal)
(rewrite <- (a = b) in goal at 2)
(simplify in goal)
(by smt)
(by atp)
(exact (p = q))
(induction n
  (case zero (by reflexivity))
  (case (succ m) (by reflexivity)))

Programmatic APIs:

• JavaScript: runTactics(state, tactics, options) returns { state, diagnostics }; rewrite(goal, eq), simplify(goal, rules), goalToTptp(...), and parseAtpStatus(...) expose the rewrite and ATP bridge helpers.
• Rust: run_tactics(state, tactics) and run_tactics_with_options(...) return TacticRunResult; rewrite(...), simplify(...), goal_to_tptp(...), and parse_atp_status(...) expose the rewrite and ATP bridge helpers.

(by smt) serializes the current goal to an SMT-LIB check by asserting the negated goal and closes the goal only when the configured solver returns unsat. Successful runs record (by smt-trusted <solver>) in the proof state. JavaScript accepts smtSolver, smtSolverArgs, and smtTimeoutMs options; Rust accepts the corresponding TacticOptions fields smt_solver, smt_solver_args, and smt_timeout_ms. The environment variables RML_SMT_SOLVER, RML_SMT_ARGS, and RML_SMT_TIMEOUT_MS provide defaults in both runtimes.

(by atp) exports the current first-order goal and local context as TPTP FOF, invokes a configured ATP path, accepts proving SZS statuses, and records (by atp-trusted <solver>) in the proof state. JavaScript accepts atpPath, atpArgs, atpName, and atpTimeoutMs options or an atp object with path, args, name, and timeoutMs; Rust accepts the corresponding TacticOptions.atp fields.

The built-in tactic set is reflexivity, symmetry, transitivity, induction, suppose, introduce, by, rewrite, simplify, smt, atp, and exact. Failed tactics emit E039 diagnostics that include the current goal.

Type Queries

# Type check: (expr of Type) — returns 1 (true) or 0 (false)
(? (zero of Natural))            # -> 1
(? (Natural of Type))            # -> 1

# Type inference: (type of expr) — returns the type name
(? (type of zero))               # -> Natural

Paradox Resolution in the Type System

In classical type theory, Type : Type leads to Russell's paradox. ADL handles this differently — paradoxes are resolved to the midpoint truth value (0.5), not rejected:

(Type: Type Type)
(s: s is s)
((s = false) has probability 0.5)
(? (s = false))                  # -> 0.5 (paradox resolves to midpoint)
(? (not (s = false)))            # -> 0.5 (fixed point of negation)
(? (Type of Type))               # -> 1   (self-referential type works)

This means ADL can serve as a meta-theory for both classical and non-classical type systems, since it can express and reason about constructs that would be inconsistent in traditional frameworks.

Built-in Operators

• =: Equality (checks assigned probability, then structural equality, then numeric comparison with decimal precision)
• !=: Inequality (defined as not = by default)
• not: Logical negation — mirrors around the midpoint of the range (1 - x in [0,1]; -x in [-1,1])
• and: Conjunction (average by default, configurable)
• or: Disjunction (maximum by default, configurable)
• +: Addition (decimal-precision)
• -: Subtraction (decimal-precision)
• *: Multiplication (decimal-precision)
• /: Division (decimal-precision, returns 0 on division by zero)

Examples

Example .lino files are available in the shared root examples/ directory. They are executed by both the JavaScript and the Rust implementations, and the canonical outputs every implementation must reproduce live in examples/expected.lino — itself written in Links Notation, so the contract between the two implementations is expressed in the same language as the examples. Examples progress from standard, familiar logic systems to more advanced and non-standard constructions.

Classical Logic (Boolean, 2-valued)

See examples/classical-logic.lino — the most familiar logic system where every proposition is either true or false:

(valence: 2)
(and: min)
(or: max)

(p: p is p)
((p = true) has probability 1)

(? (p = true))                          # -> 1 (true)
(? (not (p = true)))                    # -> 0 (false)
(? ((p = true) or (not (p = true))))    # -> 1 (law of excluded middle)
(? ((p = true) and (not (p = true))))   # -> 0 (law of non-contradiction)

For reusable imports, see lib/classical/core.lino, which packages these Boolean connectives plus excluded middle, double negation, De Morgan laws, and natural-deduction rule schemas under the classical namespace.

Propositional Logic (Probabilistic)

See examples/propositional-logic.lino — multiple propositions with standard probabilistic connectives:

(and: product)              # P(A ∩ B) = P(A) * P(B)
(or: probabilistic_sum)     # P(A ∪ B) = 1 - (1-P(A))*(1-P(B))

((rain = true) has probability 0.3)
((umbrella = true) has probability 0.6)

(? ((rain = true) and (umbrella = true)))   # -> 0.18
(? ((rain = true) or (umbrella = true)))    # -> 0.72
(? (not (rain = true)))                     # -> 0.7

Fuzzy Logic (Continuous)

See examples/fuzzy-logic.lino — standard Zadeh fuzzy logic where truth values represent degrees of membership:

(and: min)
(or: max)

((a = tall) has probability 0.8)
((b = tall) has probability 0.3)

(? ((a = tall) and (b = tall)))   # -> 0.3  (min)
(? ((a = tall) or (b = tall)))    # -> 0.8  (max)
(? (not (a = tall)))              # -> 0.2  (complement)

Ternary Kleene Logic (3-valued)

See examples/ternary-kleene.lino — Kleene's strong three-valued logic:

(valence: 3)
(and: min)
(or: max)

(? (0.5 and 1))          # -> 0.5  (unknown AND true = unknown)
(? (0.5 and 0))          # -> 0    (unknown AND false = false)
(? (0.5 or 1))           # -> 1    (unknown OR true = true)
(? (0.5 or (not 0.5)))   # -> 0.5  (law of excluded middle FAILS!)

In Kleene logic, the law of excluded middle (A ∨ ¬A) is not a tautology — this is the key difference from classical logic.

Belnap's Four-Valued Logic

See examples/belnap-four-valued.lino — extends classical logic with both...and (contradiction) and neither...nor (gap) composite natural language operators that alter the AND operation. This is the standard framework for reasoning about paradoxes:

(and: min)
(or: max)

(? (both true and false))     # -> 0.5  (contradiction: avg of 1 and 0)
(? (neither true nor false))  # -> 0    (gap: product of 1 and 0)
(? (both true and true))      # -> 1    (agree: avg of 1 and 1)

# The liar paradox resolves naturally via "both"
(s: s is s)
((s = false) has probability 0.5)
(? (s = false))               # -> 0.5

See: Belnap's four-valued logic

Liar Paradox Resolution

The liar paradox ("this statement is false") is irresolvable in classical 2-valued logic. In many-valued logics (ternary and above), it resolves to the midpoint of the range — the fixed point of negation.

See examples/liar-paradox.lino — resolution in [0, 1] range:

(s: s is s)

((s = false) has probability 0.5)
(? (s = false))          # -> 0.5  (50% from 0% to 100%)
(? (not (s = false)))    # -> 0.5  (fixed point: not(0.5) = 0.5)

See examples/liar-paradox-balanced.lino — resolution in [-1, 1] range:

(range: -1 1)
(s: s is s)

((s = false) has probability 0)
(? (s = false))          # -> 0   (0% from -100% to 100%)
(? (not (s = false)))    # -> 0   (fixed point: not(0) = 0)

Custom Operators (avg semantics)

See examples/demo.lino — demonstrates the configurable nature of operators with avg-based AND:

(a: a is a)
(!=: not =)
(and: avg)     # non-standard: average instead of min
(or: max)

((a = a) has probability 1)
((a != a) has probability 0)

(? ((a = a) and (a != a)))   # -> 0.5
(? ((a = a) or  (a != a)))   # -> 1

See examples/flipped-axioms.lino — demonstrates that the system handles arbitrary probability assignments:

(a: a is a)
(!=: not =)
(and: avg)
(or: max)

((a = a) has probability 0)
((a != a) has probability 1)

(? ((a = a) and (a != a)))   # -> 0.5 (same result — avg is symmetric)

Bayesian Inference

RML natively supports Bayesian inference and Bayesian networks. Links notation naturally describes networks of any complexity — each node's probability is a link, and joint/marginal probabilities are computed using the product and probabilistic_sum aggregators.

See examples/bayesian-inference.lino — Bayes' theorem applied to medical diagnosis (directed: Disease → Test Result):

# P(Disease) = 0.01, P(Positive|Disease) = 0.95, P(Positive|~Disease) = 0.05
# Bayes' theorem: P(Disease|Positive) = P(Pos|D)*P(D) / P(Pos)

(? (0.95 * 0.01))                                        # -> 0.0095
(? ((0.95 * 0.01) + (0.05 * 0.99)))                     # -> 0.059
(? ((0.95 * 0.01) / ((0.95 * 0.01) + (0.05 * 0.99))))  # -> 0.161017

See examples/bayesian-network.lino — a directed acyclic Bayesian network (DAG) with product and probabilistic_sum aggregators:

(and: product)              # P(A ∩ B) = P(A) * P(B)
(or: probabilistic_sum)     # P(A ∪ B) = 1 - (1-P(A))*(1-P(B))

(((cloudy) = true) has probability 0.5)
(((rain) = true) has probability 0.5)

(? (((cloudy) = true) and ((rain) = true)))   # -> 0.25 (joint)
(? (((cloudy) = true) or ((rain) = true)))    # -> 0.75 (union)

Markov Chains with Dependent Probabilities

RML can model Markov chains where transition probabilities depend on the current state. Using arithmetic and the law of total probability, multi-step state evolution is computed naturally.

See examples/markov-chain.lino — a weather model with directed transitions (today → tomorrow):

# Transition matrix: P(Sunny→Sunny)=0.8, P(Rainy→Sunny)=0.4
# Initial: P(Sunny)=0.7, P(Rainy)=0.3

# One-step: P(Sunny at t+1) = P(S→S)*P(S) + P(R→S)*P(R)
(? ((0.8 * 0.7) + (0.4 * 0.3)))   # -> 0.68
(? ((0.2 * 0.7) + (0.6 * 0.3)))   # -> 0.32

# Joint probability using product aggregator
(and: product)
(? (0.8 and 0.7))                  # -> 0.56

Markov Networks (Cyclic Graphs)

As the structural opposite of acyclic Bayesian networks, RML can also model Markov networks (Markov random fields) — undirected graphs where cycles are allowed. In links notation, undirected edges are represented as bidirectional link pairs, preserving the fundamental directionality of links.

See examples/markov-network.lino — a cyclic social influence model (Alice—Bob—Carol—Alice):

(and: product)
(or: probabilistic_sum)

(((alice) = agree) has probability 0.7)
(((bob) = agree) has probability 0.5)
(((carol) = agree) has probability 0.6)

# Pairwise joints (cycle: Alice—Bob—Carol—Alice)
(? (((alice) = agree) and ((bob) = agree)))          # -> 0.35
(? (((carol) = agree) and ((alice) = agree)))        # -> 0.42

# Three-way clique
(? (and ((alice) = agree) ((bob) = agree) ((carol) = agree)))  # -> 0.21

Self-Reasoning (Meta-Logic)

As a meta-logic, RML can reason about its own logic system and compare it with other logics.

See examples/self-reasoning.lino:

(Type: Type Type)
(Logic: Type Logic)
(RML: Logic RML)

(((RML supports_many_valued) = true) has probability 1)
(? ((RML supports_many_valued) = true))   # -> 1
(? (RML of Logic))                        # -> 1
(? (type of RML))                         # -> Logic

Testing

Both implementations have matching tests:

# JavaScript
cd js && npm test

# Rust
cd rust && cargo test

The test suites cover:

• Tokenization, parsing, and quantization
• Evaluation logic and operator aggregators
• Many-valued logics: unary, binary (Boolean), ternary (Kleene), quaternary, quinary, higher N-valued, and continuous (fuzzy)
• Both [0, 1] and [-1, 1] ranges
• Truth constants (true, false, unknown, undefined): defaults, redefinition, range changes, use in expressions, quantization
• Belnap operators (both...and, neither...nor): default aggregators, redefinition, composite/prefix/infix forms, fuzzy values, range changes
• Liar paradox resolution across logic types
• Decimal-precision arithmetic (+, -, *, /) and numeric equality
• Dependent type system: universes, Pi-types, lambdas, application, definitional equality, type queries, prefix type notation
• Link-based tactic engine: reflexivity, symmetry, transitivity, induction, suppose, introduce, by, rewrite, simplify, exact
• Self-referential types: (Type: Type Type), paradox resolution alongside types, coexistence with universe hierarchy
• Bayesian inference: Bayes' theorem, law of total probability, conditional probability, complement rule
• Bayesian networks: joint probability (product), probabilistic sum (probabilistic_sum), multi-node networks, chain rule decomposition
• Self-reasoning: meta-logic properties, comparing logic systems, paradox resolution in meta context
• Markov chains: one-step and multi-step transitions, joint probability, stationary distribution, conditional transitions with links
• Markov networks: cyclic graphs, pairwise joints, three-way cliques, clique potentials, normalization
• Automatic sequences: a Pecan-style domain plugin that decides thue-morse-cube-free
• Comprehensive valence coverage: 0 (continuous), 1 (unary), 2–10, 100, 1000, with both ranges
• English-readability lint: identifier shape, operator-only links, allow-list (see English-readability lint)

API

See language-specific documentation:

• JavaScript API
• Rust API

Diagnostics

Both implementations expose an evaluate() entry point that returns a list of results plus structured diagnostics — every parser, evaluator, and type checker error carries a stable code (E001, …), a message, and a 1-based source span. The CLIs print them as file:line:col: Exxx: message with a caret under the offending token. See docs/DIAGNOSTICS.md for the full code list and usage examples.

English-readability lint

Every link in examples/ (and, when introduced, lib/) is expected to read as an English sentence. A small lint script enforces the conventions:

node scripts/lint-english.mjs --allowlist scripts/lint-english.allowlist.json examples/*.lino
# or, from the JS package:
(cd js && npm run lint:english)

The lint reports two classes of violation in file:line:col: code: message form (the same shape used by structured diagnostics):

• identifiers-without-hyphens — identifiers that combine multiple words with _ or camelCase instead of kebab-case. The lint suggests the hyphenated form (e.g. wet_grass → wet-grass).
• operator-only-link — an operator definition such as (@: + -) whose body contains no English word. The lint suggests adding a word-form alternative (e.g. (equals: =), (plus: +)).

Reserved RML/LiNo vocabulary (and, or, not, is, has, probability, true, false, unknown, Type, lambda, …) is never flagged, and single-word identifiers (alice, cloudy, Natural) are accepted as-is.

Allow-list

For deliberate exceptions, scripts/lint-english.allowlist.json accepts two arrays:

{
  "identifiers": ["legacy_name"],
  "links": ["demo.lino:5"]
}

Identifiers in identifiers are silenced wherever they appear; entries in links are keyed by <basename>:<line> and silence the operator-only-link rule for that specific definition. CI runs the lint with this file so any new violation fails the build.

References

• Many-valued logic — overview of logics with more than two truth values
• Boolean algebra — classical 2-valued logic
• Three-valued logic — ternary logics (Kleene, Łukasiewicz, Bochvar)
• Łukasiewicz logic — N-valued and infinite-valued extensions
• Fuzzy logic — continuous-valued logic with degrees of truth
• Balanced ternary — ternary system using {-1, 0, 1}
• Four-valued logic (Belnap) — extends classical logic with "both" (contradiction) and "neither" (gap)
• Liar paradox — "this statement is false" and its resolution in many-valued logics
• Bayesian statistics — probability as a measure of belief
• Bayesian inference — updating beliefs based on evidence
• Bayesian network — probabilistic graphical models
• Bayes' theorem — relating conditional and marginal probabilities
• Markov chain — stochastic model with state-dependent transitions
• Law of total probability — computing marginal probabilities from conditionals

License

See LICENSE file.