ed/manual_slop
Private
Public Access
0
0
Fork 0
Code Activity

conductor(deob_lexicon_v2): Reshape Maps 1, 2, 3 in dedup_map.md

Browse Source 
3 principled maps reshaped per v2 corrections.

Map 1 (Curry-Howard): proof/construction distinction preserved; construction is a sub-type tag, not a replacement (per user 2026-06-23).

Map 2 (Types=Kinds, v2): Removed the 'Sets' leg (set is a data structure, not an enumerable type). Documented that 'kind' (lowercase) is reserved for enumeration types: components, DAG nodes, fat structs. Type/Genus/Kind are analogous (per user 2026-06-23).

Map 3 (Procedures=Words, v2): Removed the 'Functions' leg. function (declarative/math) and procedure (imperative/CS) are distinct concepts (per user 2026-06-23).

Maps 4, 5, 6 unchanged.
This commit is contained in:
Edward R. Gonzalez
2026-06-23 20:00:23 -04:00
parent 5cd8a277d5
commit 014179aa71
1 changed files with 40 additions and 19 deletions
Download Patch File Download Diff File Expand all files Collapse all files
conductor/tracks/video_analysis_deob_lexicon_20260621/dedup_map.md
+40 -19
View File
@@ -18,15 +18,17 @@
**Origin.** Howard, 1969 — "The formulae-as-types notion of construction." The Curry-Howard correspondence says a proof of proposition `P` corresponds to a program of type `P`. The user has adopted this as the principled foundation.
**The map.**
**The map (v2, refined).**
| Conventional | Principled re-encoding | Why it dedups |
|---|---|---|
| "we have a proof that x² ≥ 0" | `construction (x : Real) -> square(x) >= zero(Real) : Prop` | The "proof" is a program; the "proposition" is a type. |
| "we have a proof that x² ≥ 0" | `proof (x : Real) -> square(x) >= zero(Real) : Prop` (with `construction` as sub-type tag when the proof is constructive) | The "proof" is a program; the "proposition" is a type. |
| "the proof of the theorem" | `the program (lambda.x. proof_body) : Prop` | Same. |
| "a proof by induction" | `a recursive construction` | The induction principle is recursion. |
| "a proof by induction" | `a recursive construction` (the `construction` tag applies) | The induction principle is recursion. |
| "QED" | `(result : Prop)` | The "QED" is the value of the program. |
**v2 refinement (per user 2026-06-23):** "a construction is a type of proof." The v1 map collapsed `proof → construction`; v2 removes the collapse. The principled form keeps `proof` as the main term; `construction` is applied as a sub-type tag when the proof is constructive. See L5 in `V2_CHANGELOG.md`.
**Edge cases:**
1. **Classical logic (excluded middle, double negation):** the principled map preserves them as classical programs (via continuations or CPS transform). The user prefers constructive; the LLM should flag classical logic and offer the constructive alternative.
@@ -37,53 +39,72 @@
---
## Map 2: Sets = Kinds = Types (constructive) `[principled]`
## Map 2: Types = Kinds (constructive, "kind" reserved for enums) `[principled]`
**Source cluster:** Cluster 3 (Type Theory — `kind`/`type` distinction); Cluster 4 (Lambda Calculus — `Data` type); Cluster 7 (`Notiones.txt` — `Type = "successful act of association"`).
**Origin.** Per Martin-Löf, 1975 — "An intuitionistic theory of types." The constructive type theory identification of sets, kinds, and types. The user has adopted this as the principled foundation.
**Origin.** Per Martin-Löf, 1975 — "An intuitionistic theory of types." The constructive type theory identification of types and kinds. The user has adopted this as the principled foundation.
**The map.**
**The map (v2, refined).**
| Conventional | Principled re-encoding | Why it dedups |
|---|---|---|
| "the set of natural numbers" | `kind Nat = Zero | Succ(Nat)` | The "set" is a kind; the "kind" is a type. |
| "the set of pairs (A, B)" | `kind Pair<A, B> = (A, B)` | Same. |
| "the set of functions A → B" | `kind Function<A, B> = (A) -> B` | Same. |
| "x is in the set S" | `x : S` | The "in" relation is type ascription. |
| "for all x in S, P(x)" | `forall x : S, P(x) : Prop` | The "for all in" is dependent quantification. |
| "the type of natural numbers" | `Type Nat = Zero | Succ(Nat)` | The "type" is a kind. |
| "the type of pairs (A, B)" | `Type Pair<A, B> = (A, B)` | Same. |
| "the type of functions A → B" | `Type Function<A, B> = (A) -> B` | Same. |
| "x is in the type T" | `x : T` | The "in" relation is type ascription. |
| "for all x in T, P(x)" | `forall x : T, P(x) : Prop` | The "for all in" is dependent quantification. |
| "the enum of cases" (NEW v2) | `kind Cases = Case1 | Case2 | Case3` | The "kind" is reserved for enumeration types. |
**v2 refinement (per user 2026-06-23):** "Set is a specific data structure, not directly related to an enumerable type. Do not reencode set as a kind. ... Type/Genus/Kind are analogous no need to reencode. Type and Type of types is analogous to kind. Kind is useful term to reserve for enumeration types, especially when used with components, DAG nodes, or fat structs."
The v1 map collapsed `set → kind`; v2 removes the collapse. The v2 map identifies:
- `Type` = the type (the conventional term, no re-encoding)
- `Kind` = type-of-types (capital K, standard)
- `kind` (lowercase) = reserved for enumeration types (components, DAG nodes, fat structs)
The "set" leg of the v1 map is removed; `set` is a specific data structure (HashSet, SortedSet, etc.), not an enumerable type. See L1, L8 in `V2_CHANGELOG.md`.
**Edge cases:**
1. **Naive set theory (comprehension axiom):** the principled map excludes comprehension (it leads to Russell's paradox). The user is constructive; the LLM should flag comprehension and offer the constructive alternative.
2. **ZFC set theory:** the user is not ZFC; the LLM should preserve ZFC if the reader is using it, but offer the constructive form.
3. **Class/set distinction (proper classes):** the principled map collapses this; the LLM should preserve the distinction if the reader needs it.
4. **The data structure `set`:** the v2 map treats `set` as a data structure (HashSet, SortedSet, etc.) without re-encoding. The LLM should not conflate `set` (data structure) with `kind` (enumeration type).
**User-specific additions:** none. This map is fully principled.
---
## Map 3: Functions = Procedures = Words (concatenative) `[principled]`
## Map 3: Procedures = Words (concatenative) `[principled]`
**Source cluster:** Cluster 2 (University Notes — pseudo-code with explicit procedures); Cluster 4 (Lambda Calculus — `Application (algorithim, input)`); Cluster 9 (Chapter 1.sectr — `proc` keyword for procedures).
**Origin.** Forth (1968), ColorForth (Chuck Moore), and the concatenative programming tradition. The identification of functions, procedures, and words (concatenative language terms). The user has adopted this as the principled foundation.
**Origin.** Forth (1968), ColorForth (Chuck Moore), and the concatenative programming tradition. The identification of procedures and words (concatenative language terms). The user has adopted this as the principled foundation.
**The map.**
**The map (v2, refined).**
| Conventional | Principled re-encoding | Why it dedups |
|---|---|---|
| "the function f(x) = x + 1" | `procedure f (x : Real) -> Real : x + 1` | The "function" is a procedure; the procedure is a word. |
| "apply the function to the input" | `apply (procedure, input) -> result` | The "apply" is a word. |
| "compose the functions" | `compose (f, g) -> h where h(x) = f(g(x))` | The "compose" is a word. |
| "the function's body" | `the procedure's body` | Same. |
| "call the function" | `execute the procedure` | The "call" is "execute" in the concatenative tradition. |
| "the procedure f(x) = x + 1" | `procedure f (x : Real) -> Real : x + 1` | The "procedure" is a word. |
| "apply the procedure to the input" | `apply (procedure, input) -> result` | The "apply" is a word. |
| "compose the procedures" | `compose (f, g) -> h where h(x) = f(g(x))` | The "compose" is a word. |
| "the procedure's body" | `the procedure's body` | (no change) |
| "call the procedure" | `execute the procedure` | The "call" is "execute" in the concatenative tradition. |
| "the function f(x) = x + 1" (NEW v2) | **NO RE-ENCODING** (clarify with etymology; function = declarative/math, procedure = imperative/CS) | Function is a distinct concept (mathematical, declarative); procedure is a distinct concept (CS, imperative). |
**v2 refinement (per user 2026-06-23):** "A procedure is not necessarily a function, a function has a specific declarative sense it, a procedure is imperative." The v1 map collapsed `function → procedure`; v2 removes the collapse. The v2 map identifies:
- `procedure` = imperative (CS, concatenative)
- `function` = declarative (math)
These are distinct concepts; the LLM should not collapse them. See L2 in `V2_CHANGELOG.md`.
**Edge cases:**
1. **Pure functions (no side effects):** the principled map preserves them. Concatenative languages can be pure (e.g., Kitten, Joy).
2. **First-class functions:** the principled map preserves them. Procedures are first-class values.
3. **Higher-order functions:** the principled map preserves them as procedures that return procedures.
4. **Mathematical functions (declarative):** the v2 map treats them as a distinct concept (math, declarative). The LLM should preserve the `function` term for math, not collapse to `procedure`.
**User-specific additions:** none. This map is fully principled.