╭
𝟙𝟠·
logic I've ‘discovered’ the field of Mathematics called Finite Model Theory! Model Theory includes, and is introduced with, a focus on infite structures, so I put it
┊
on the future pile - logic pencil puzzles are finite. But Finite Model Theory looks relevant - it is likely over my head, but I'll dig in a bit and see if I can
┊
connect any dots to my playground.
┊
┊
𝟙𝟞·
puzzles To even solve the trivial Slitherlink Puzzle (a 1×1 puzzle with a single ‘4’) semi-symbolically, I'm going to have to up my constraint handling. My plan was
┊
to support constraint expressions - special objects which give some information about an otherwise indeterminate value.
┊
┊
My choice was to wrap a logical formula (another expression) using the variable ‘_’ to represent the constraint expression. This could get unweildy, so in practice I
┊
have kept them simple enough to be useful for my current, puzzle-solving purposes.
┊
┊
As an example, if x is ‘_∈{1 2}’ and y is ‘_∈{2 7}’ we can deduce ‘x+y’ will satisfy the constraint ‘_∈{3 4 8 9}’and we could also deduce from ‘x=y’ that ‘x=y=2’. The
┊
pigeonholer I implemented to solve Sudoku puzzles in ⟪Silver⟫ starts with ‘_∈{1⋯9}’ for blank squares and 27 9-way not-equal expressions using an n-ary ‘¬=’ operator.
┊
The handling is not Sudoku specific - I'm hoping it will work for a few more puzzles before I tidy things up.
┊
┊
Which brings me back to the start - I didn't implement constraint expressions properly, and now that I'm counting the number of edges around a square that are on the
┊
path, I have to do at least some tidying.
┊
┊
𝟙𝟞·
Some online news source or other asked if AI could create anything original... (continued)
𝕁
┊
𝕒
┊
𝟙𝟝·
I don't know how to address the political situation here in the US... (continued)
𝕟
┊
𝕒
┊
puzzles with formulas defining 10 different puzzle types. Nikoli, the company that popularized “Number Place” puzzles under the Japanese trademark ‘Sudoku’, publishes
𝕣
┊
collections in Japan and describes each on their website:
𝕪
┊
┊
┊
As I get my ⟪Silver⟫ Solver working on each, I'll post my ⟪Sapphire⟫ definitions.
┊
┊
𝟘𝟡·
coding I often pass keyword parameters to a subroutine unchanged, and ended up with alot of ‘keyword=keyword’ code in Python function calls. Reserving ‘=’ for the
┊
equality predicate (I just replace ‘=’ with ‘==’ when generating Python or C) I instead use ‘→’ to pass keyword parameters - ‘keyword→7’. I added a postfix operator
┊
‘→←’ to pass the value of the variable as the keyword, so I can abbreviate ‘keyword→keyword’ ·as ‘keyword→←’.
┊
┊
𝟘𝟠·
logic I've added ‘comprehensions’ which support set and sequence expressions such as { _^3 ⋮ 1⋯2026} and ⟨ ⦗str _⦘ ⋮ x y z ⟩, where the variable ‘_’ (displayed as ◒
┊
in logical contexts, to satisfy my aesthic preferences) which is evaluated for each of the elements to the right of the ‘⋮’ symbol. I use ‘⋯’ as an inclusive, integer
┊
range operator, so ⟨1⋯3⟩ is the tuple ⟨1 2 3⟩. It meshes well with my implementation of sets of integers expressed as intervals.
┊
┊
𝟘𝟠·
coding I've been on a side trip to additional ‘rational’ code generation based on syntactic analysis rather than ad-hoc text manipulation. This next stage let me
┊
translate operators (‘⊗’ and ‘⊙’ for cross and dot-product) into calls to generic functions, but there's more work to make it remotely robust.
┊
┊
𝟘𝟝·
puzzles I started on a formulation of Slitherlink rules in ⟪Sapphire⟫. Connectivity, as a pairwise relation could be easily satisfied by being true for any vertices
┊
that are connected to anything. I ended up defining a distance function with a special value (rather than a distinct relation) for ‘not connected’. In the next day or
╰
two, I'll see how ⟪Silver⟫ does trying to find a satisfying model (aka solution).
╭
𝟛𝟘·
coding I've been bogged down by my bootstrapping shenanigans. I finally decided to re-execl the current build when cyclic dependencies could change generated code.
┊
Because I'm building my tools in place, I use a “revert-bootstraps” routine often to deal with all-to-frequent breakage.
┊
┊
𝟚𝟠·
coding More language infrastructure progress - I've got code generating from the ⟪Violet⟫ language layer that bridges between ⟪Cobalt⟫ (aka C) and ⟪Midnight⟫ (aka
┊
Python). I generate code that uses Python's ‘ctypes’ module to call C from Python, making it easy to mix and match implementations.
┊
┊
𝟚𝟞·
coding I took a small step toward sensible language handling by generating a full parse tree for a small input file. Starting life as a no-op, my evolving ‘zypp’
┊
preprocessor converts ⟪Midnight⟫ and ⟪Cobalt⟫ to Python and C, respectively, in an entirely ad-hoc fashion. At least I know I can create an inviting bug hotel.
┊
Eventually, each language layer I use will share a unified parser, but different intermediate code generators which will perform first level semantic checks. The
┊
intermiedate language will support high level primitives that can be lowered to target subsets which can be used to emit code. My ⟪Sapphire⟫ project has a good deal
┊
of infrastructure to cope with.
┊
𝔻
┊
𝟚𝟝·
piward I finished implementing SDL ‘framebuffer’ objects which display a screen sized OpenGL texture. Framebuffer support is primarily for debugging, but also can be
𝕖
┊
used with small ‘gadget’ displays, like Pimoroni's Display Hat Mini, ePaper displays, also available from Pimoroni or from Waveshare, which I used to prototype a
𝕔
┊
Raspberry Pi based e-Reader.
𝕖
┊
𝕞
┊
𝟚𝟜·
bonfire I finally got around to watching Jordan Peele's documentary "Get Out" the other night. I have to say, the re-enactments were grisly, but well done.
𝕓
┊
𝕖
┊
𝟚𝟛·
logic I've added support for the Cartesian Product, represented by ‘×’ in Unicode (U+D7). What I call “tuple constrained quantification” (∀⟨x y⟩∈Z×Z) is accepted in
𝕣
┊
⟪Sapphire⟫ as well as set exponentiation by an integer (Z^4 ▷ Z×Z×Z×Z) ({1⋯3}^3 ▷ {1⋯3}×{1⋯3}×{1⋯3}). Finite expressions can be evaluated in calculator fashion (⟨1 2
┊
3⟩∈{1⋯3}^3 ▷ ✔) (∀⟨a b⟩∈{1⋯3}^2 a>3 ⇒ a+b>4 ▷ ✔) and can also be symbolically manipulated by ⟪Ag⟫, aka “The Silver Solver”. I've updated my Sudoku rules to use these
┊
new features
┊
┊
𝟚𝟚·
coding I'm using ‘⊙‘ for dot product and ‘⊗’ for cross product. My preprocessor translates these from binary operators into calls to ‘dot’ and ‘cross’, which are
┊
native in GLSL and implemented in Python to work on number sequences of equal length (dot) or only 3-tuples of numbers (cross).
┊
┊
𝟚𝟚·
coding While I use Unicode extensively and appreciate its near universal adoption and support, I object to any description of it as a "character set". [continued]
┊
┊
𝟚𝟙·
coding I updated my color text routines that I use in all my Python tools to proceess faster when read into Emacs. One day, I may create an IDE for my ‘neo-retro’
┊
logic-puzzle computing environment, but Emacs is still the best tool for me.
┊
╰
𝟘𝟞·
logic I now have a somewhat general "pigeonhole solver" ...