25 August 2026 1201et FRANK

A session with my discrete algebra playground program

Goal is a MATLAB/Mathematica-style REPL for interactively exploring, in discrete math, the construction of binary operations closed over a finite domain.

Initially coded by Claude Fable 5, prompted with imaginary transcripts demonstrating user interactions I wanted the software to support.

Subsequent feature requests and bug fixes handled by Claude Sonnet 4.8, followed by my most recent major feature request to local AI Qwen 3.8 for "aggressively proactive derivation by process of elimination." Qwen 3.8 was impressive at understanding the codebase and figuring out where to make changes and additions to implement the feature.

% ./run-workbench.sh
Discrete math workbench.  Ctrl-D to exit.

Here are commands I understand:
  S = {a, b, c}                      -- define a set
  declare * such that S x S --> S    -- declare a binary operation with domain/codomain S
  * is associative                   -- assert a property (associative, commutative)
  c is an identity under *           -- assert an element is a two-sided identity
  c is a left-identity under *       -- assert an element is a left- or right-identity
  * has a unique left-identity       -- constrain how many left-/right-identities * has
  * has 2 left-identities            -- exactly N left-/right-identities
  * has at least 1 right-identity    -- at least N left-/right-identities
  * has at most 2 right-identities   -- at most N left-/right-identities
  a * b = c                          -- define a table entry
  redefine a * b = c                 -- force-redefine an entry
  undefine a * b                     -- remove an entry
  table(*)                           -- show the Cayley table
  possibilities(*)                   -- show each undefined cell's contradiction-free candidates
  inventory                          -- show everything defined so far
  a * b                              -- query an expression
  save session.txt                   -- save the session to a file
  load session.txt                   -- load a session from a file
--> S = {a, b, c, d}
Set S created with 4 members: a, b, c, d.
--> declare associative @ such that S @ S --> S
Binary operation @ created with domain S x S, range S
Asserting that @ is associative: 64 constraint instances added.
--> @ has at least 1 left-identity
OK. Asserting that @ has at least 1 left-identity.
--> @ has at least 1 right-identity
OK. Asserting that @ has at least 1 right-identity.
--> inventory
We have:
A set S with 4 members: a, b, c, d.
A binary operation @ with domain S x S and range S,
where
@ is associative.
--> table(@)
@ as a lookup table:

x @ y          y

    @   a   b   c   d
      +---+---+---+---+
    a | ' | ' | ' | ' |
      +---+---+---+---+
 x  b | ' | ' | ' | ' |
      +---+---+---+---+
    c | ' | ' | ' | ' |
      +---+---+---+---+
    d | ' | ' | ' | ' |
      +---+---+---+---+

where blank entries have yet to be defined,
and entries marked ' are partially constrained.
@ is associative.
--> a @ a = b
OK. Defining @ so a @ a = b
--> table(@)
@ as a lookup table:

x @ y          y

    @   a   b   c   d
      +---+---+---+---+
    a | b | ' | ' | ' |
      +---+---+---+---+
 x  b | ' | ' | ' | ' |
      +---+---+---+---+
    c | ' | ' | ' | ' |
      +---+---+---+---+
    d | ' | ' | ' | ' |
      +---+---+---+---+

where blank entries have yet to be defined,
and entries marked ' are partially constrained.
@ is associative.
--> c @ a = d
OK. Defining @ so c @ a = d
--> d @ a = a
OK. Defining @ so d @ a = a
This determines the following facts:
c @ b = a  by Associativity(c,a,a)
d @ b = b  by Associativity(d,a,a)
a @ c = d  by process of elimination
a @ d = a  by process of elimination
b @ a = c  by process of elimination
b @ b = d  by process of elimination
b @ c = a  by process of elimination
b @ d = b  by process of elimination
c @ c = b  by process of elimination
c @ d = c  by process of elimination
d @ c = c  by process of elimination
d @ d = d  by process of elimination
a @ b = c  by process of elimination
@ is now fully defined!
@ has a unique left-identity: d.
@ has a unique right-identity: d.
@ is commutative.
@ has left-cancellation.
@ has right-cancellation.
Looks like d is a left-identity!
Looks like d is a right-identity!
--> table(@)
@ as a lookup table:

x @ y          y

    @   a   b   c   d
      +---+---+---+---+
    a | b | c | d | a |
      +---+---+---+---+
 x  b | c | d | a | b |
      +---+---+---+---+
    c | d | a | b | c |
      +---+---+---+---+
    d | a | b | c | d |
      +---+---+---+---+

@ is associative.
d is an identity.
--> inventory
We have:
A set S with 4 members: a, b, c, d.
A binary operation @ with domain S x S and range S,
where
@ is associative.
d is an identity.
a @ a = b
c @ a = d
d @ a = a
--> save Frank01.session.txt
Saved 8 commands to Frank01.session.txt.
--> undefine d @ a
OK. d @ a is now undefined, and no longer a
d is no longer a left-identity.
d is no longer a right-identity.
--> table(@)
@ as a lookup table:

x @ y          y

    @   a   b   c   d
      +---+---+---+---+
    a | b | ' | ' | ' |
      +---+---+---+---+
 x  b | ' | ' | ' | ' |
      +---+---+---+---+
    c | d | ' | ' | ' |
      +---+---+---+---+
    d | ' | ' | ' | ' |
      +---+---+---+---+

where blank entries have yet to be defined,
and entries marked ' are partially constrained.
@ is associative.
--> ^D

Sessions can be saved as plain text human-readable transcripts:

% cat Frank01.session.txt
Discrete math workbench.  Ctrl-D to exit.
--> S = {a, b, c, d}
Set S created with 4 members: a, b, c, d.

--> declare @ such that S @ S --> S
Binary operation @ created with domain S x S, range S

--> @ is associative
OK. Asserting that @ is associative: 64 constraint instances added.

--> @ has at least 1 left-identity
OK. Asserting that @ has at least 1 left-identity.

--> @ has at least 1 right-identity
OK. Asserting that @ has at least 1 right-identity.

--> a @ a = b
OK. Defining @ so a @ a = b

--> c @ a = d
OK. Defining @ so c @ a = d

--> d @ a = a
OK. Defining @ so d @ a = a
This determines the following facts:
c @ b = a  by Associativity(c,a,a)
d @ b = b  by Associativity(d,a,a)
a @ c = d  by process of elimination
a @ d = a  by process of elimination
b @ a = c  by process of elimination
b @ b = d  by process of elimination
b @ c = a  by process of elimination
b @ d = b  by process of elimination
c @ c = b  by process of elimination
c @ d = c  by process of elimination
d @ c = c  by process of elimination
d @ d = d  by process of elimination
a @ b = c  by process of elimination
@ is now fully defined!
@ has a unique left-identity: d.
@ has a unique right-identity: d.
@ is commutative.
@ has left-cancellation.
@ has right-cancellation.
Looks like d is a left-identity!
Looks like d is a right-identity!

-->

Session transcripts can be played back into the REPL using the 'load' command:

% ./run-workbench.sh
Discrete math workbench.  Ctrl-D to exit.

Here are commands I understand:
  S = {a, b, c}                      -- define a set
  declare * such that S x S --> S    -- declare a binary operation with domain/codomain S
  * is associative                   -- assert a property (associative, commutative)
  c is an identity under *           -- assert an element is a two-sided identity
  c is a left-identity under *       -- assert an element is a left- or right-identity
  * has a unique left-identity       -- constrain how many left-/right-identities * has
  * has 2 left-identities            -- exactly N left-/right-identities
  * has at least 1 right-identity    -- at least N left-/right-identities
  * has at most 2 right-identities   -- at most N left-/right-identities
  a * b = c                          -- define a table entry
  redefine a * b = c                 -- force-redefine an entry
  undefine a * b                     -- remove an entry
  table(*)                           -- show the Cayley table
  possibilities(*)                   -- show each undefined cell's contradiction-free candidates
  inventory                          -- show everything defined so far
  a * b                              -- query an expression
  save session.txt                   -- save the session to a file
  load session.txt                   -- load a session from a file
--> inventory
Blank slate.
--> load Frank01.session.txt
Loading Frank01.session.txt
--> S = {a, b, c, d}
Set S created with 4 members: a, b, c, d.
--> declare @ such that S @ S --> S
Binary operation @ created with domain S x S, range S
--> @ is associative
OK. Asserting that @ is associative: 64 constraint instances added.
--> @ has at least 1 left-identity
OK. Asserting that @ has at least 1 left-identity.
--> @ has at least 1 right-identity
OK. Asserting that @ has at least 1 right-identity.
--> a @ a = b
OK. Defining @ so a @ a = b
--> c @ a = d
OK. Defining @ so c @ a = d
--> d @ a = a
OK. Defining @ so d @ a = a
This determines the following facts:
c @ b = a  by Associativity(c,a,a)
d @ b = b  by Associativity(d,a,a)
a @ c = d  by process of elimination
a @ d = a  by process of elimination
b @ a = c  by process of elimination
b @ b = d  by process of elimination
b @ c = a  by process of elimination
b @ d = b  by process of elimination
c @ c = b  by process of elimination
c @ d = c  by process of elimination
d @ c = c  by process of elimination
d @ d = d  by process of elimination
a @ b = c  by process of elimination
@ is now fully defined!
@ has a unique left-identity: d.
@ has a unique right-identity: d.
@ is commutative.
@ has left-cancellation.
@ has right-cancellation.
Looks like d is a left-identity!
Looks like d is a right-identity!
Loaded 8 commands from Frank01.session.txt.
-->