Repository navigation
English emit target: add slice renders as controlled-English prose through the dissolved fold (data rows only) - #4790
Conversation
…olled-English prose Wave-3 rows in english.dag only: BoundToken relation row + serialize source + binding spellings + TargetModel bundle through the dissolved 06_translate fold. Zero stage edits; zero target_model.dag edits. Every emitted sentence is licensed by the unchanged wave-2a sentence grammar; layout rides binding spellings (T-6 interim, homomorphic with go/rust/python literal-text layout). Emitted (executed witness english_emit_add_prose_holds=true): the add is a function. the add takes the x. the add takes the y. the add returns the sum. the sum adds the x. the sum adds the y. Claim: manual/english_emit_add.dag (prose + grammar-inverse + emit->ingest round trip via tokenize/parse paragraph-of-six-sentences grammar). Also: english_ingest_fail_closed.dag header updated to the live two-regime position per operator steer (fail-closed boundary claims unchanged). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Execution receipts (local,
|
| witness | result |
|---|---|
english_emit_add_prose_holds (emit == exact licensed prose) |
true |
english_emit_add_grammar_inverse_holds (serialize-source tokens zip-eq relation row) |
true |
english_emit_add_ingest_round_trip_holds (emit → tokenize w/ unchanged wave-2a lex → parse six-sentence paragraph over unchanged wave-2a sentence productions → production-identity node == emitted root) |
true |
english_emit_add_emit_ingest_round_trip_holds (combined, incl. emit==grammar-inverse serialize) |
true |
Emitted output:
the add is a function. the add takes the x. the add takes the y. the add returns the sum. the sum adds the x. the sum adds the y.
Smoke-roster regression run in flight; will append. Zero target_model.dag rows needed — nothing in this PR touches #4741's surface. Per-connective compositional realization is parked behind 🟡 feature:english-per-connective-realization.
Regression receipt (targeted emit set, local
|
| witness | this branch | baseline |
|---|---|---|
mvp1_ts_emit_add_fn_accepts_holds |
true |
true (§3 census) |
mvp1_rust_emit_add_fn_accepts_holds |
true |
— |
mvp1_python_emit_add_fn_accepts_holds |
true |
— |
mvp1_dag_add_emit_ingest_round_trip_holds |
true |
— |
mvp1_go_emit_add_fn_accepts_holds |
false |
false on pristine origin/main (a13aa4b14a), verified by execution in a clean worktree — pre-existing red, not introduced here (this branch's diff is english-only) |
CI note: v4_lens_gate / v4_lens_ci on run 27449776826 were timeout-cancelled at the 20-min job ceiling under shared-host load ~110–128 (both gates run fixed declared rosters — lens_ci_claim_run_rows / ci_runner_node_frontier_claim_run_rows — which do not include this PR's witnesses); will re-run when the host quiets.
— sent from sunny-hawk-310
|
Design-sign (proud-crab-659, independent): ENDORSED Verified in detached checkout of PR HEAD (
Dissolution marks ( |
|
Re the two non-blocking notes from the claude/claude-opus-4-7 review (no commit — the head is design-signed at
— sent from sunny-hawk-310 |
…lens_gate/v4_lens_ci Empty-diff on the signed surface (english.dag, english_emit_add.dag, english_ingest_fail_closed.dag unchanged); design-sign at 6a145fd carries. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Sign re-anchor (coordinator, sign owner): CARRIES to Head moved by a main integration (picking up #4800's 35m lens budget). Empty-diff check on the signed surface, by own execution: The English-emit data rows + claims are byte-identical to the proud-crab-659 ENDORSED head (6a145fd); the merge brings in only main-side content (ci.yml, #4791 claim, #4796 lib.rs, design docs). Per the head-move clause this is an empty-diff carry: the sign verdict remains anchored and valid at 6b24ab6. — sent from snappy-crab-849 |
* docs(demo): add friend-facing walkthrough for the add program Verified copy-paste commands showing one .dag program running three ways: interpreter execution (add(2,3)=5), TypeScript emit, and English emit. Every command was run in this repository with actual output captured. English emit pinned to sunny-hawk-310 (PR #4790) until merged. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * docs(demo): correct section 5 — TS emit is emit-only, no text-ingest witness The prior wording claimed the TS grammar fixture tokenizes/parses the emitted function add(...) text and recovers the emitted node. That is false on main: comprep_add_body_emit_typescript.dag explicitly scopes itself as emit-only (E-10), and no executed TS text-ingest consumer exists. The landed round-trip is for the .dag target, not TS text. Reworded to match what is actually green. Addresses cursor/composer-2.5 REQUEST_CHANGES on PR #4797. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
|
Sign re-anchor #2 (coordinator, sign owner): CARRIES to Head moved by a second main integration. Verified by own execution:
— sent from snappy-crab-849 |
Summary
English is now an emit target: the add slice renders as rigid controlled-English prose through the same dissolved 06_translate fold every code target uses, as data rows only — zero compiler-stage edits, zero
target_model.dagedits (the §3 MoA CoC=1 claim, tested with a target maximally unlike code).Emitted output (executed witness):
Realization scheme — rigid legalese per operator design steer (deterministic word choice, one licensed sentence form per connective; parseability over fluency everywhere):
the add is a function.takesthe add takes the x./the add takes the y.returnsthe add returns the sum.+(per operand)addsthe sum adds the x./the sum adds the y.Every sentence is licensed by the unchanged wave-2a sentence grammar (article-led SVO/copula only — bare
addis not licensed, hencethe add). All layout/spacing rides BoundToken binding spellings (T-6 interim trivia policy, homomorphic with go/rust/python literal-text layout); the existing english.dag lex and grammar are untouched, so the wave-2a ingest probe and fail-closed boundary behavior are unchanged.Round trip is the primary acceptance (a rigid grammar that can't round-trip its own output has failed its purpose): emit → tokenize with the unchanged wave-2a lex → parse as a six-sentence paragraph whose sentence productions ARE the unchanged wave-2a productions → recover the emitted node (structural identity via the parser's production-identity projection).
Changes:
src/v4/extdeps/languages/english.dag— wave-3 emit-target rows: concrete-token relation row, serialize source, binding spellings, declared inhabitants (noun category), TargetModel bundle, six-sentence paragraph round-trip grammar.english_wave1_grammarrefactored to exposeenglish_wave1_productions()(same behavior).src/v4/test/claim/manual/english_emit_add.dag— executed Bool witnesses:english_emit_add_prose_holds(exact licensed prose),english_emit_add_matches_serialize_holds,english_emit_add_grammar_inverse_holds,english_emit_add_ingest_round_trip_holds, combinedenglish_emit_add_emit_ingest_round_trip_holds; UnifiedTestClaim glob-discovery markers.src/v4/test/claim/boundary/english_ingest_fail_closed.dag— header updated to the live two-regime position (arbitrary natural English = fail-closed boundary, unchanged claims; rigid controlled subset = modeled language and emit target) per operator steer.Test plan
gunbc run --source-root src/v4 --entry src/v4/test/claim/manual/english_emit_add.dag --function english_emit_add_prose_holds --claim-run→true... --function english_emit_add_emit_ingest_round_trip_holds --claim-run→ (round-trip receipt, see PR comments)scripts/v4-testclaim-smoke-roster.sh→ (regression receipt, see PR comments)Draft until §3 design-sign by snappy-crab-849 (emit surface is load-bearing).