╭
𝟚𝟟·
In trying to add expressive set comprehensions to ⟪Sapphire⟫, it's hard to avoid Russell's Paradox. Expressed in ⟪Sapphire⟫ extended with unrestricted quantifiers it
┊
would be expressed as ‘∃x ∀y y∈x≡y¬∈y’. The restrictions I want to place on quantifiers complicate things, and with Python-like comprehensions as values, it get's
┊
even more complicated. Lots to think about.
┊
┊
𝟚𝟘·
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.
┊
┊
𝟙𝟠·
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.
┊
┊
𝟘𝟠·
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.
╭
𝟚𝟛·
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
𝕔
┊
┊
𝟘𝟞·
I now have a somewhat general "pigeonhole solver" which, given a set of equations of the form x_i¬=x_j and for each x_i, one equation of the form x_i∈{c_j c_(j+1)
┊
c_(j+2) ... c_(j+k)}. This can directly be solved with a search, but I've been trying to avoid that in my pretense toward symbolic manipulation. In the end, I'm not
╰
sure my approach is all that different than a search - if I can write my approach up in a sensible form, I'll post a doc someplace and hope to learn more.
𝟳
/
𝟘𝟚·
This page is a rough (perhaps embarrassingly so) version of a solution to the first puzzle in Raymond M. Smullyan's Satan, Cantor and Infinity
𝟲
/
𝟛𝟘·
I'm generalizing the way I validate proof steps so inference rules match if any formulae with an equivalent (Sapphire specific) normal form would have matched.