associative-dependent-logic

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

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 176 tests and produce identical results.

For implementation details, see ARCHITECTURE.md.

Overview

ADL (Associative-Dependent Logic) 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
• 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

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/adl-links.mjs demo.lino

Rust

cd rust
cargo run -- demo.lino

Example

Create a file example.lino:

# Define a term
(a: a is a)

# Set up operators
(!=: not =)
(and: avg)
(or: max)

# Assign probabilities to axioms
((a = a) has probability 1)
((a != a) has probability 0)

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

Output:

0.5
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.

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
true	1	1	max(range)
false	0	-1	min(range)
unknown	0.5	0	(max(range) - min(range)) / 2 + min(range)
undefined	0.5	0	(max(range) - min(range)) / 2 + min(range)

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])

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

When the range changes (via (range: ...)), 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: prod)  # Product
(and: ps)    # Probabilistic sum: 1 - (1-p1)*(1-p2)*...

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

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

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 both js/ and rust/ directories.

Standard Logic (with avg semantics)

See demo.lino:

(a: a is a)
(!=: not =)
(and: avg)
(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

Flipped Axioms

See flipped-axioms.lino — demonstrates that the system can handle 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
(? ((a = a) or  (a != a)))   # -> 1

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)
(!=: not =)
(and: avg)
(or: max)

((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)
(!=: not =)
(and: avg)
(or: max)

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

Ternary Kleene Logic

See examples/ternary-kleene.lino — demonstrates Kleene's strong three-valued logic where AND=min, OR=max:

(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 0))           # -> 0.5  (unknown OR false = unknown)
(? (not 0.5))            # -> 0.5  (NOT unknown = unknown)
(? (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.

Testing

Both implementations have 176 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
• Liar paradox resolution across logic types
• Decimal-precision arithmetic (+, -, *, /) and numeric equality
• Dependent type system: universes, Pi-types, lambdas, application, type queries, prefix type notation
• Self-referential types: (Type: Type Type), paradox resolution alongside types, coexistence with universe hierarchy

API

See language-specific documentation:

• JavaScript API
• Rust API

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}
• Liar paradox — "this statement is false" and its resolution in many-valued logics

License

See LICENSE file.