From c8b871572ef24be552c437987cc14c20105b31d1 Mon Sep 17 00:00:00 2001 From: Faried Abu Zaid Date: Thu, 13 Aug 2026 23:45:28 +0200 Subject: [PATCH] Say what the sentence-under-connective fix actually fixed The entry read "Sentence markers that dropped the structure's alphabet", which is the smaller half of it and reads like a detail. The bigger half is that 3.1.0 CRASHED: checked against the v3.1.0 tag, (all x.(Eq(x,x))) & (all x.(Eq(x,x))) -> IndexError (all x.(Eq(x,x))) & Lt(y,z) -> IndexError so a sentence could not appear as an operand of a connective at all, nor beside an open formula. That shipped, which makes it a fix users can act on rather than an internal tidy-up, and the changelog now says so along with why: a sentence evaluates to the all/none marker rather than to a relation with tapes, so placing it in an enclosing formula is not a tape renaming, and for two sentences there is no tape to rename to. Co-Authored-By: Claude Opus 5 --- CHANGELOG.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 53d7793..6c6f8d7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -149,8 +149,18 @@ relation on every presentation. - **Serializing such a presentation.** JSON has no tuples, so a reloaded product alphabet was a set of lists (unhashable) and the padding symbol a list. Both are restored on load, on both engines. +- **A sentence as an operand of a connective raised `IndexError`.** In 3.1.0, + `check('(all x.(Eq(x,x))) & (all y.(Lt(y,y)))')` crashed, and so did a + sentence placed beside an open formula. A sentence has no free variables, so + it evaluates to the all/none *marker* — an automaton non-empty exactly when + the sentence is true — rather than to a relation with tapes. Placing that + into an enclosing formula is therefore not a tape renaming, and with two + sentences there is no tape to rename to at all. Fixed on both engines, and + pinned across all four binary connectives, nested, and on either side of an + open formula. +- Sentence markers that dropped the structure's alphabet, which made the + marker's language wrong for the enclosing query. - A universal quantifier that silently became an existential. -- Sentence markers that dropped the structure's alphabet. - Relation automata are restricted to the universe on *every* tape, not all but the last: a relation that still held of a non-element made universal sentences false on encodings that were not elements at all.