newish musings
blog logic puzzles piward coding the-bonfire
github profile
𝟚𝟛· coding The transition to treating constraints as a class of ⟪Iron⟫ Interpreter internal values has been... slow. I make a mess when I'm exploring to find a solution
or implementation that works and meets my design goals. Breaking changes are a time to consolidate the current design before going forward... I was too focused on
getting to the next exploration - constraints as first class values, and, well, messed up.
𝟚𝟘· logic By encoding logic pencil puzzles, rules and instances, in ⟪Sapphire⟫ I define a CSP (Constraint Satisfaction Problem) and ⟪Silver⟫ is my ad-hoc solver. My
⟪Iron⟫ interpreter can, when an expression would be undefined with eager evaluation, return a meta-object, referencing the only partially evaluated expression. These
can be interpreted as errors by the environment, but are used by Silver to find solutions: an assertion such as ‘x=5+7’ might not be evaluated past ‘x=12’ if ‘x’ is
completely unkown, but can be fully resolved by commiting ‘x’ in the solution to be ‘12’. If ‘y’ is undefined, ‘y∈{3 12 15}’ won't be evaluated, but can be used as a
constraint on ‘y’ in the solution. These, combined with an assertion that ‘x=y’ yields the solution ‘x=12 ∧ y=12’.
Previously, I didn't allow constraints to be passed around as a ‘first class’ meta-value with ⟪Silver⟫ relied almost on re-evaluating the current unresolved
assertions with various ‘resolution’ steps that reconcile constraints. Now constraints can be passed as values, and carry, along with information what the domain
value could be, but also information about the source of the constraint. As an example, given ‘x∈{1 2 3}’ and ‘y∈{3 4 5}’ as constraints, ‘x+y’ can be evaluated to
the constraint ‘x+y∈{4⋯8}’ which, returned as a meta-value means ‘x+y<10’ can be evaluted to true.
This can't eliminate the need for specialized resolution steps, like my ⟪Silver⟫ pigeonholer, but the hope is that they can be kept simple and orthogonal to be used,
along with extended evaluation, as primitive steps in a search.
Lazy evaluation, if I want to use it for optimization or expressiveness, will hopefully be follow as a relatively straightforward extension of all this.
𝟚𝟘· the-bonfire The Trump Adminstration's demands for lists of Jewish Faculty from educational institutions is a not only a potential danger to those faculty members
given past and recent history, but even a list for ‘special protection’ is unlawful: the use of Congressionally allocated funds to defend or support Jewish Faculty
violates the 1st Amendment's establishment clause. LDS Members, Muslims, Sikhs, Buddhists, Hindus, Spiritualists, Atheists, Wiccans, Scientologists and more have
experienced persecution on American campuses. Any government protection from religious persecution must defend all belief systems and not be biased by political
motivation.
𝟙𝟡· the-bonfire The title of Robert Wachter's recent article... (continued)
𝟙𝟠· the-bonfire I was updating my rant about how Unicode is poorly suited for use as a character set in computing when I realized it is a real solid start to an open
standard in word processing. The addition of emoji makes communication so much clearer: 🇺🇸/🇬🇱=🙀
𝟙𝟠· 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 The paper “Mathematical Definition and Systematization of Puzzle Rules” by Itsuki Maeda and Yasuhiro Inoue details a mathematical framework for logic pencil
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:
Slitherlink Sudoku Shikaku Choco Banana Inshi no Heya Fillomino Kurotto Sukoro Norinori Hitori.
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" ...