nelumbo.logic

Level: nelumbo.logic. Available after import nelumbo.logic, or transitively through any package (nelumbo.integers and up).

The logic module. A file gets it with import nelumbo.logic, or transitively by importing any package. It declares the Boolean type, the three Boolean values, the connectives, lambdas, the quantifiers (which are lambdas), equality, and the three top-level forms (fact, <=>, ?).

Source: src/main/resources/org/modelingvalue/nelumbo/logic/logic.nl

Import:

import nelumbo.logic

nelumbo.logic itself imports nelumbo.lang, which contributes the meta-syntax — import, ::, ::=, ::>, type-variable declarations, <NAME>, <STRING>, etc. (see lang.nl).

Types

Boolean   :: Object
Function  :: Object
Literal   :: Object
Struct    :: Object

• Boolean — the type of truth-valued expressions.
• Literal — values that are their own canonical form: named constants such as T1, Hendrik, true, integers, strings, …
• Function — values produced by functional patterns (e.g., a+b, fib(n), r(x/y)) that reduce by rules.
• Struct — values that are constructors with structural equality: two Struct values are equal when their parts are (collection literals such as {1,2} and [1,2] are Structs; a user type declared :: Struct gets the same). They take the eq route like a Literal.

The Literal / Function split is what makes the rules in Equality (below) sufficient: every operand of = is either a literal, a function, or a variable, and the rules cover the relevant cases.

Boolean values

Boolean ::= true       @nelumbo.logic.NBoolean,
            false      @nelumbo.logic.NBoolean,
            unknown    @nelumbo.logic.NBoolean

Three Boolean values, all bound to the native class NBoolean. unknown is a first-class value of type Boolean, not an absence of one. See three-valued-logic.md for the truth tables.

Connectives

-> and <-> are not native. They are defined in Nelumbo on top of ! and |:

Boolean p1, p2

p1 -> p2   <=>  !p1 | p2
p1 <-> p2  <=>  (p1 -> p2) & (p2 -> p1)

This is the meta-language working on itself: <-> is a user-level rule built from ->, which is itself a user-level rule built from native | and !.

logicTest.nl is the executable truth-table specification for all five connectives, including the unknown rows. For example:

unknown & true   ? [..][..]
unknown & false  ? [][()]
true -> unknown  ? [..][..]
false -> unknown ? [()][]

Quantifiers

Boolean ::= E<Lambda<Boolean>>   @nelumbo.logic.ExistentialQuantifier,
            A<Lambda<Boolean>>   @nelumbo.logic.UniversalQuantifier

• E[x](p) — there exists x such that p.
• A[x](p) — for all x, p.
• Up to six bound variables are allowed: E[x,y,z](p), A[x,y,z](p); a seventh is a parse error.
• The quantified variables range over a type whose extent is unknown: Nelumbo never tries every member of the type. E[x](p) and A[x](p) are decided only by what p derives for x (through =, a lookup from a bound argument, or x in a known collection), so E[x](q(x)) over a fact q(Piet) is unknown. See The open world.

The quantifier is the keyword E / A followed by a lambda whose body is a Boolean: [x,y](p) is a Lambda2<…,Boolean>. The bracketed variables must be declared variables, they are local to the body, and the body is at the lowest precedence (#0) so the entire expression inside the parentheses is consumed. (The quantifiers used to carry their own <(> <Variable#100> <,> , <)+> variable-list pattern; they now share the lambda syntax.)

Test examples from logicTest.nl:

Test :: Object
Test ::= T1, T2
Test a

E[a](a=T1 | a=T2)      ? [()][]
A[a](a=T1 & a=T2)      ? [][()]
!A[a](a!=T1 & a!=T2)   ? [()][]
!E[a](a!=T1 | a!=T2)   ? [][()]

Equality

private Boolean ::= eq(<Literal>, <Literal>)   @nelumbo.logic.Equal

Boolean ::= <one Object> = <one Object>   #30   @nelumbo.logic.NIs,
            <Object> != <Object>           #30

Two related but distinct primitives:

• eq(l1, l2) is the private literal-equality predicate. It compares two Literal values directly and is bound to the native class Equal. Importers never call eq themselves.
• <one Object> = <one Object> is the public equality operator, bound to NIs. Unlike eq, it accepts any Object on either side, so it works on functions and variables as well as literals.

!= has no native binding of its own; it is the negation of =. The remaining cases are rules, written with intersection types {A,B} ("both an A and a B") over a generic parameter E:

Type E
E            n1, n2
{E,Literal}  l1, l2
{E,Function} f1, f2

l1 = l2   <=>  eq(l1, l2)
l1 = f1   <=>  f1 = l1
n1 != n2  <=>  !(n1 = n2)
f1 = f2   <=>  E[l1](f1 = l1 & f2 = l1)

• l1 = l2 — two literals (of one type E) are compared by eq.
• l1 = f1 swaps a literal-equals-function query into function-equals-literal form, so that user-defined rules of the shape f1 = literal <=> ... are reachable from either direction.
• f1 = f2 — two functions are equal when some literal is equal to both.

one: equality has a single answer

Both holes of = are unique holes (<one Object>): a variable on either side of = gets at most one value. This is what gives every function a single result:

• fib(5)=f must give exactly one closed answer [(f=5)][..] (or none). A rule that derives two values, or one value with an open facts side, is reported as Inconsistent result: ... has non unique bindings.
• A function value asserted as a fact is closed: after fact m(Beatrix)=Juliana, m(Beatrix)=x gives [(x=Juliana)][..] and m(Beatrix)=Beatrix is false. All other facts are open (unknown when not asserted), so = on functions is the main source of closed answers over facts.
• Only a variable in the hole is constrained, not a term: m(x)=Juliana may have many answers (m need not be injective), and x=y with both unbound is not checked.

= is what makes ordinary rule bodies work — f=fib(n-1)+fib(n-2) succeeds when both sides reduce to the same value — and is the surface form used in queries to bind variables. Note that a class-less Object functor with arguments is Function-typed, so f(1)=f(1) is undecided unless the result type is declared :: Struct (structural equality).

Top-level forms

nelumbo.logic also declares the three statement forms that appear at the top level of a .nl file:

Root ::= "fact" <(> <Boolean#0> <,> , <)+>                                       @nelumbo.logic.Fact,
         <Boolean#0> "<=>" <(> <Boolean#0> <(> "if" <Boolean#0> <)?> <,> , <)+>   @nelumbo.logic.Rule,
         <Boolean#0> ? <(> <BINDING> <BINDING> <)?>                               @nelumbo.logic.Query

The fact keyword is required: a bare Boolean at top level is rejected. The BINDING fragment that follows ? is a named pattern, declared here:

pattern BINDING ::= [ <(> <(> ( <(> <Variable#100> = <Object#0> <,> , <)*> ) <|> .. <)> <,> , <)*> ]

That is the grammar of [(a=T1), (a=T2)], [..], [], and combinations such as [(a=0),..]. (It was previously a stand-alone Binding :: Object type; it is now a named pattern, so it adds no type — it is pure syntax for the query suffix.) See test-expression-semantics.md for how a ? test is judged to pass or fail.

Exports summary

After import nelumbo.logic, the following are visible to the importer:

eq is private and is not visible to importers.

See also

• three-valued-logic.md — the semantic model these operators live in
• lambdas.md — the [x](body) values the quantifiers and the collection operations take
• operators.md — full operator catalogue
• writing-rules.md — <=> and if semantics
• logicTest.nl — executable specification of every connective and quantifier