commit 6f513293ca930a0733f64305fb1063f45966352c Author: milner Date: Tue Sep 22 09:20:00 2026 +0200 initial commit: confluence and normalisation diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e8eff97 --- /dev/null +++ b/.gitignore @@ -0,0 +1,11 @@ +_build/ +*.vo +*.vok +*.vos +*.glob +*.aux +*.cmi +*.cmo +*.cmx +__pycache__/ +*.pyc diff --git a/README.md b/README.md new file mode 100644 index 0000000..408c869 --- /dev/null +++ b/README.md @@ -0,0 +1,15 @@ +This was (mostly) me being bored in a Monday evening and in an attempt to formalise in Rocq the confluence and normalisation results that Delia Kesner and Shane Ó Conchúir obtain for the lambda calculus of Milner with partial substitutions which is available as arXiv:2312.13270. + +## Graphs + +The dependency graph covers the six milestones and every edge runs from a dependency to the result that uses it while the node colour encodes the status proved or stated or planned or blocked: + +![Theorem dependency graph](graphs/dependency.svg) + +The rule sketch gives the transition system generated by the rules B and Gc and R: + +![Reduction rules](graphs/rules.svg) + +The reduction graph gives the bounded reduct set of the term that applies the duplicating identity to a variable with every edge labelled by its rule and with the normal form marked: + +![Reduction graph of the duplicating identity](graphs/reduction.svg) diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..0eacd23 --- /dev/null +++ b/dune-project @@ -0,0 +1,4 @@ +(lang dune 3.21) +(name lambda_sub) +(using rocq 0.11) +(version 0.1.0) diff --git a/graphs/dependency.dot b/graphs/dependency.dot new file mode 100644 index 0000000..8efbe20 --- /dev/null +++ b/graphs/dependency.dot @@ -0,0 +1,110 @@ +digraph theorem_deps { + rankdir=LR; + bgcolor="white"; + node [fontname=Inter, fontsize=10, fontcolor="#333333"]; + edge [fontname=Inter, fontsize=8, color="#333333"]; + graph [fontname=Inter, fontsize=12, labelloc=t, label="Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M0)"]; + subgraph cluster_M0 { + label="M0"; + style="rounded"; + color="#bbbbbb"; + fontcolor="#333333"; + exec_step [label="exec_step", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#333333", tooltip="exec_step theory/ExecReducer.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + exec_examples [label="exec_examples", color="#38761d", fillcolor="#d9ead3", style="filled", fontcolor="#333333", tooltip="exec_examples theory/ExecReducer.v https://arxiv.org/html/2312.13270v1", shape=ellipse]; + } + subgraph cluster_M1 { + label="M1"; + style="rounded"; + color="#bbbbbb"; + fontcolor="#333333"; + m1_syntax [label="M1 syntax/binding", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m1_syntax (section 2) https://arxiv.org/html/2312.13270v1", shape=ellipse]; + m1_open_close [label="open/close laws", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m1_open_close (section 2) https://arxiv.org/html/2312.13270v1", shape=ellipse]; + m1_red1 [label="red1 (B, Gc, R)", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m1_red1 (section 2) https://arxiv.org/html/2312.13270v1", shape=ellipse]; + } + subgraph cluster_M2 { + label="M2"; + style="rounded"; + color="#bbbbbb"; + fontcolor="#333333"; + lemma_2_1_fv_preserved [label="Lemma 2.1 fv preserved", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_2_1_fv_preserved (section 2) https://arxiv.org/html/2312.13270v1", shape=box]; + lemma_2_2_full_comp [label="Lemma 2.2 full composition", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_2_2_full_comp (section 2) https://arxiv.org/html/2312.13270v1", shape=box]; + lemma_2_3_beta_sim [label="Lemma 2.3 β-simulation", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_2_3_beta_sim (section 2) https://arxiv.org/html/2312.13270v1", shape=box]; + } + subgraph cluster_M3 { + label="M3"; + style="rounded"; + color="#bbbbbb"; + fontcolor="#333333"; + m3_measure [label="sub measure", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m3_measure (section A) https://arxiv.org/html/2312.13270v1", shape=ellipse]; + m3_termination [label="{R,Gc} termination", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m3_termination (section 3.1) https://arxiv.org/html/2312.13270v1", shape=box]; + m3_local_confluence [label="{R,Gc} local confluence", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m3_local_confluence (section 3.1) https://arxiv.org/html/2312.13270v1", shape=box]; + lemma_3_2_sub_nf_unique [label="Lemma 3.2 sub NF unique", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="lemma_3_2_sub_nf_unique (section 3.1) https://arxiv.org/html/2312.13270v1", shape=box]; + } + subgraph cluster_M4 { + label="M4"; + style="rounded"; + color="#bbbbbb"; + fontcolor="#333333"; + m4_par [label="parallel reduction par", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m4_par (section 3.2) https://arxiv.org/html/2312.13270v1", shape=ellipse]; + m4_par_diamond [label="par diamond", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m4_par_diamond (section 3.2) https://arxiv.org/html/2312.13270v1", shape=box]; + theorem_confluence_terms [label="Confluence on terms", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="theorem_confluence_terms (section 3.2) https://arxiv.org/html/2312.13270v1", shape=box]; + } + subgraph cluster_M5 { + label="M5"; + style="rounded"; + color="#bbbbbb"; + fontcolor="#333333"; + m5_mvar [label="XΔ metaterms", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_mvar (section 3.3) https://arxiv.org/html/2312.13270v1", shape=ellipse]; + m5_rx [label="RX rule", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_rx (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box]; + m5_eq_C [label="=C setoid", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_eq_C (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box]; + m5_coherence [label="RX + =C coherence", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m5_coherence (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box]; + theorem_confluence_metaterms [label="Confluence on metaterms", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="theorem_confluence_metaterms (section 3.3) https://arxiv.org/html/2312.13270v1", shape=box]; + } + subgraph cluster_M6 { + label="M6"; + style="rounded"; + color="#bbbbbb"; + fontcolor="#333333"; + m6_translation [label="translation to λβp", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_translation (section 4) https://arxiv.org/html/2312.13270v1", shape=box]; + m6_sn [label="SN for simply typed", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_sn (section 6) https://arxiv.org/html/2312.13270v1", shape=box]; + m6_intersection [label="intersection typing", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_intersection (section 6) https://arxiv.org/html/2312.13270v1", shape=box]; + m6_typable_sn [label="typable → SN", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_typable_sn (section 6) https://arxiv.org/html/2312.13270v1", shape=box]; + m6_sn_typable [label="SN → typable", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="m6_sn_typable (section 6) https://arxiv.org/html/2312.13270v1", shape=box]; + corollary_6_21_psn [label="Cor 6.21 PSN", color="#777777", fillcolor="#f3f3f3", style="dashed", fontcolor="#333333", tooltip="corollary_6_21_psn (section 6) https://arxiv.org/html/2312.13270v1", shape=box]; + } + exec_step -> exec_examples; + exec_examples -> m1_syntax; + m1_syntax -> m1_open_close; + m1_syntax -> m1_red1; + m1_open_close -> m1_red1; + m1_red1 -> lemma_2_1_fv_preserved; + m1_red1 -> lemma_2_2_full_comp; + m1_red1 -> lemma_2_3_beta_sim; + lemma_2_2_full_comp -> lemma_2_3_beta_sim; + m1_red1 -> m3_measure; + m3_measure -> m3_termination; + m3_termination -> m3_local_confluence; + m1_red1 -> m3_local_confluence; + m3_local_confluence -> lemma_3_2_sub_nf_unique; + m1_red1 -> m4_par; + lemma_3_2_sub_nf_unique -> m4_par; + m4_par -> m4_par_diamond; + m4_par_diamond -> theorem_confluence_terms; + lemma_2_3_beta_sim -> theorem_confluence_terms; + m1_syntax -> m5_mvar; + m5_mvar -> m5_rx; + m1_red1 -> m5_rx; + m5_mvar -> m5_eq_C; + m5_rx -> m5_coherence; + m5_eq_C -> m5_coherence; + lemma_3_2_sub_nf_unique -> m5_coherence; + m5_coherence -> theorem_confluence_metaterms; + m4_par_diamond -> theorem_confluence_metaterms; + m1_red1 -> m6_translation; + m6_translation -> m6_sn; + m6_sn -> m6_intersection; + m6_intersection -> m6_typable_sn; + m6_typable_sn -> m6_sn_typable; + m6_sn_typable -> corollary_6_21_psn; + theorem_confluence_terms -> corollary_6_21_psn; +} diff --git a/graphs/dependency.png b/graphs/dependency.png new file mode 100644 index 0000000..e60c57a Binary files /dev/null and b/graphs/dependency.png differ diff --git a/graphs/dependency.svg b/graphs/dependency.svg new file mode 100644 index 0000000..971167a --- /dev/null +++ b/graphs/dependency.svg @@ -0,0 +1,493 @@ + + + + + + +theorem_deps + +Milner's Lambda-Calculus with Partial Substitutions - theorem dependency (M0) + +cluster_M0 + +M0 + + +cluster_M1 + +M1 + + +cluster_M2 + +M2 + + +cluster_M3 + +M3 + + +cluster_M4 + +M4 + + +cluster_M5 + +M5 + + +cluster_M6 + +M6 + + + +exec_step + + +exec_step + + + + + +exec_examples + + +exec_examples + + + + + +exec_step->exec_examples + + + + + +m1_syntax + + +M1 syntax/binding + + + + + +exec_examples->m1_syntax + + + + + +m1_open_close + + +open/close laws + + + + + +m1_syntax->m1_open_close + + + + + +m1_red1 + + +red1 (B, Gc, R) + + + + + +m1_syntax->m1_red1 + + + + + +m5_mvar + + +XΔ metaterms + + + + + +m1_syntax->m5_mvar + + + + + +m1_open_close->m1_red1 + + + + + +lemma_2_1_fv_preserved + + +Lemma 2.1 fv preserved + + + + + +m1_red1->lemma_2_1_fv_preserved + + + + + +lemma_2_2_full_comp + + +Lemma 2.2 full composition + + + + + +m1_red1->lemma_2_2_full_comp + + + + + +lemma_2_3_beta_sim + + +Lemma 2.3 β-simulation + + + + + +m1_red1->lemma_2_3_beta_sim + + + + + +m3_measure + + +sub measure + + + + + +m1_red1->m3_measure + + + + + +m3_local_confluence + + +{R,Gc} local confluence + + + + + +m1_red1->m3_local_confluence + + + + + +m4_par + + +parallel reduction par + + + + + +m1_red1->m4_par + + + + + +m5_rx + + +RX rule + + + + + +m1_red1->m5_rx + + + + + +m6_translation + + +translation to λβp + + + + + +m1_red1->m6_translation + + + + + +lemma_2_2_full_comp->lemma_2_3_beta_sim + + + + + +theorem_confluence_terms + + +Confluence on terms + + + + + +lemma_2_3_beta_sim->theorem_confluence_terms + + + + + +m3_termination + + +{R,Gc} termination + + + + + +m3_measure->m3_termination + + + + + +m3_termination->m3_local_confluence + + + + + +lemma_3_2_sub_nf_unique + + +Lemma 3.2 sub NF unique + + + + + +m3_local_confluence->lemma_3_2_sub_nf_unique + + + + + +lemma_3_2_sub_nf_unique->m4_par + + + + + +m5_coherence + + +RX + =C coherence + + + + + +lemma_3_2_sub_nf_unique->m5_coherence + + + + + +m4_par_diamond + + +par diamond + + + + + +m4_par->m4_par_diamond + + + + + +m4_par_diamond->theorem_confluence_terms + + + + + +theorem_confluence_metaterms + + +Confluence on metaterms + + + + + +m4_par_diamond->theorem_confluence_metaterms + + + + + +corollary_6_21_psn + + +Cor 6.21 PSN + + + + + +theorem_confluence_terms->corollary_6_21_psn + + + + + +m5_mvar->m5_rx + + + + + +m5_eq_C + + +=C setoid + + + + + +m5_mvar->m5_eq_C + + + + + +m5_rx->m5_coherence + + + + + +m5_eq_C->m5_coherence + + + + + +m5_coherence->theorem_confluence_metaterms + + + + + +m6_sn + + +SN for simply typed + + + + + +m6_translation->m6_sn + + + + + +m6_intersection + + +intersection typing + + + + + +m6_sn->m6_intersection + + + + + +m6_typable_sn + + +typable → SN + + + + + +m6_intersection->m6_typable_sn + + + + + +m6_sn_typable + + +SN → typable + + + + + +m6_typable_sn->m6_sn_typable + + + + + +m6_sn_typable->corollary_6_21_psn + + + + + diff --git a/graphs/reduction.dot b/graphs/reduction.dot new file mode 100644 index 0000000..2115012 --- /dev/null +++ b/graphs/reduction.dot @@ -0,0 +1,20 @@ +digraph reduction_dup { + rankdir=LR; + bgcolor="white"; + node [fontname=Inter, fontsize=10]; + edge [fontname=Inter, fontsize=9, color="#333333"]; + graph [labelloc=t, fontcolor="#333333", label="(lambda x. x x) y reduction graph"]; + n0 [label="(lambda x. x x) y", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"]; + n1 [label="(x x)[x/y]", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"]; + n2 [label="(y x)[x/y]", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"]; + n2b [label="(x y)[x/y]", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"]; + n3 [label="(y y)[x/y]", shape=box, style="filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"]; + nf [label="y y (normal form)", shape=doublecircle, style=filled, fillcolor="#d9ead3", color="#38761d", fontcolor="#333333"]; + n0 -> n1 [label="B", color="#990000"]; + n1 -> n2 [label="R", color="#674ea7"]; + n1 -> n2b [label="R", color="#674ea7"]; + n2 -> n3 [label="R", color="#674ea7"]; + n2b -> n3 [label="R", color="#674ea7"]; + n3 -> nf [label="Gc", color="#38761d"]; + {rank=same; n2; n2b;} +} diff --git a/graphs/reduction.png b/graphs/reduction.png new file mode 100644 index 0000000..951435e Binary files /dev/null and b/graphs/reduction.png differ diff --git a/graphs/reduction.svg b/graphs/reduction.svg new file mode 100644 index 0000000..fcb47ca --- /dev/null +++ b/graphs/reduction.svg @@ -0,0 +1,93 @@ + + + + + + +reduction_dup + +(lambda x. x x) y reduction graph + + +n0 + +(lambda x. x x) y + + + +n1 + +(x x)[x/y] + + + +n0->n1 + + +B + + + +n2 + +(y x)[x/y] + + + +n1->n2 + + +R + + + +n2b + +(x y)[x/y] + + + +n1->n2b + + +R + + + +n3 + +(y y)[x/y] + + + +n2->n3 + + +R + + + +n2b->n3 + + +R + + + +nf + + +y y (normal form) + + + +n3->nf + + +Gc + + + diff --git a/graphs/rules.dot b/graphs/rules.dot new file mode 100644 index 0000000..c0054d6 --- /dev/null +++ b/graphs/rules.dot @@ -0,0 +1,19 @@ +digraph lambda_sub_cfg { + rankdir=TB; + bgcolor="white"; + node [fontname=Inter, fontsize=10]; + edge [fontname=Inter, fontsize=9, color="#333333"]; + start [label="term", shape=oval, style=filled, fillcolor="#f3f3f3", color="#333333"]; + beta [label="(lambda x. t) u", shape=box, style="rounded,filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"]; + es [label="t[x/u]", shape=box, style="rounded,filled", fillcolor="#f5f5f5", color="#333333", fontcolor="#333333"]; + pure [label="pure term", shape=oval, style=filled, fillcolor="#f3f3f3", color="#333333"]; + nf [label="normal form", shape=doublecircle, style=filled, fillcolor="#d9ead3", color="#38761d"]; + start -> beta [label="App(Lam,_)"]; + start -> es [label="ESub"]; + start -> pure [label="BVar/FVar/Lam"]; + beta -> es [label="B", color="#990000"]; + es -> es [label="R (one occurrence)", color="#674ea7"]; + es -> pure [label="Gc (x not in fv)", color="#38761d"]; + pure -> pure [label="B under context", color="#990000"]; + es -> nf [label="R/Gc normalisation", color="#674ea7"]; +} diff --git a/graphs/rules.png b/graphs/rules.png new file mode 100644 index 0000000..cb48afa Binary files /dev/null and b/graphs/rules.png differ diff --git a/graphs/rules.svg b/graphs/rules.svg new file mode 100644 index 0000000..a051cf0 --- /dev/null +++ b/graphs/rules.svg @@ -0,0 +1,100 @@ + + + + + + +lambda_sub_cfg + + + +start + +term + + + +beta + +(lambda x. t) u + + + +start->beta + + +App(Lam,_) + + + +es + +t[x/u] + + + +start->es + + +ESub + + + +pure + +pure term + + + +start->pure + + +BVar/FVar/Lam + + + +beta->es + + +B + + + +es->es + + +R (one occurrence) + + + +es->pure + + +Gc (x not in fv) + + + +nf + + +normal form + + + +es->nf + + +R/Gc normalisation + + + +pure->pure + + +B under context + + + diff --git a/graphs/theorems.json b/graphs/theorems.json new file mode 100644 index 0000000..f36a280 --- /dev/null +++ b/graphs/theorems.json @@ -0,0 +1,272 @@ +{ + "paper": { + "title": "Milner's Lambda-Calculus with Partial Substitutions", + "authors": ["Delia Kesner", "Shane Ó Conchúir"], + "url": "https://arxiv.org/abs/2312.13270", + "html": "https://arxiv.org/html/2312.13270v1" + }, + "milestones": ["M0", "M1", "M2", "M3", "M4", "M5", "M6"], + "current": "M0", + "nodes": [ + { + "id": "exec_step", + "label": "exec_step", + "kind": "infra", + "status": "proved", + "milestone": "M0", + "section": "", + "file": "theory/ExecReducer.v", + "depends": [] + }, + { + "id": "exec_examples", + "label": "exec_examples", + "kind": "infra", + "status": "proved", + "milestone": "M0", + "section": "", + "file": "theory/ExecReducer.v", + "depends": ["exec_step"] + }, + { + "id": "m1_syntax", + "label": "M1 syntax/binding", + "kind": "infra", + "status": "planned", + "milestone": "M1", + "section": "2", + "file": "", + "depends": ["exec_examples"] + }, + { + "id": "m1_open_close", + "label": "open/close laws", + "kind": "infra", + "status": "planned", + "milestone": "M1", + "section": "2", + "file": "", + "depends": ["m1_syntax"] + }, + { + "id": "m1_red1", + "label": "red1 (B, Gc, R)", + "kind": "infra", + "status": "planned", + "milestone": "M1", + "section": "2", + "file": "", + "depends": ["m1_syntax", "m1_open_close"] + }, + { + "id": "lemma_2_1_fv_preserved", + "label": "Lemma 2.1 fv preserved", + "kind": "paper", + "status": "planned", + "milestone": "M2", + "section": "2", + "file": "", + "depends": ["m1_red1"] + }, + { + "id": "lemma_2_2_full_comp", + "label": "Lemma 2.2 full composition", + "kind": "paper", + "status": "planned", + "milestone": "M2", + "section": "2", + "file": "", + "depends": ["m1_red1"] + }, + { + "id": "lemma_2_3_beta_sim", + "label": "Lemma 2.3 β-simulation", + "kind": "paper", + "status": "planned", + "milestone": "M2", + "section": "2", + "file": "", + "depends": ["m1_red1", "lemma_2_2_full_comp"] + }, + { + "id": "m3_measure", + "label": "sub measure", + "kind": "infra", + "status": "planned", + "milestone": "M3", + "section": "A", + "file": "", + "depends": ["m1_red1"] + }, + { + "id": "m3_termination", + "label": "{R,Gc} termination", + "kind": "paper", + "status": "planned", + "milestone": "M3", + "section": "3.1", + "file": "", + "depends": ["m3_measure"] + }, + { + "id": "m3_local_confluence", + "label": "{R,Gc} local confluence", + "kind": "paper", + "status": "planned", + "milestone": "M3", + "section": "3.1", + "file": "", + "depends": ["m3_termination", "m1_red1"] + }, + { + "id": "lemma_3_2_sub_nf_unique", + "label": "Lemma 3.2 sub NF unique", + "kind": "paper", + "status": "planned", + "milestone": "M3", + "section": "3.1", + "file": "", + "depends": ["m3_local_confluence"] + }, + { + "id": "m4_par", + "label": "parallel reduction par", + "kind": "infra", + "status": "planned", + "milestone": "M4", + "section": "3.2", + "file": "", + "depends": ["m1_red1", "lemma_3_2_sub_nf_unique"] + }, + { + "id": "m4_par_diamond", + "label": "par diamond", + "kind": "paper", + "status": "planned", + "milestone": "M4", + "section": "3.2", + "file": "", + "depends": ["m4_par"] + }, + { + "id": "theorem_confluence_terms", + "label": "Confluence on terms", + "kind": "paper", + "status": "planned", + "milestone": "M4", + "section": "3.2", + "file": "", + "depends": ["m4_par_diamond", "lemma_2_3_beta_sim"] + }, + { + "id": "m5_mvar", + "label": "XΔ metaterms", + "kind": "infra", + "status": "planned", + "milestone": "M5", + "section": "3.3", + "file": "", + "depends": ["m1_syntax"] + }, + { + "id": "m5_rx", + "label": "RX rule", + "kind": "paper", + "status": "planned", + "milestone": "M5", + "section": "3.3", + "file": "", + "depends": ["m5_mvar", "m1_red1"] + }, + { + "id": "m5_eq_C", + "label": "=C setoid", + "kind": "paper", + "status": "planned", + "milestone": "M5", + "section": "3.3", + "file": "", + "depends": ["m5_mvar"] + }, + { + "id": "m5_coherence", + "label": "RX + =C coherence", + "kind": "paper", + "status": "planned", + "milestone": "M5", + "section": "3.3", + "file": "", + "depends": ["m5_rx", "m5_eq_C", "lemma_3_2_sub_nf_unique"] + }, + { + "id": "theorem_confluence_metaterms", + "label": "Confluence on metaterms", + "kind": "paper", + "status": "planned", + "milestone": "M5", + "section": "3.3", + "file": "", + "depends": ["m5_coherence", "m4_par_diamond"] + }, + { + "id": "m6_translation", + "label": "translation to λβp", + "kind": "paper", + "status": "planned", + "milestone": "M6", + "section": "4", + "file": "", + "depends": ["m1_red1"] + }, + { + "id": "m6_sn", + "label": "SN for simply typed", + "kind": "paper", + "status": "planned", + "milestone": "M6", + "section": "6", + "file": "", + "depends": ["m6_translation"] + }, + { + "id": "m6_intersection", + "label": "intersection typing", + "kind": "paper", + "status": "planned", + "milestone": "M6", + "section": "6", + "file": "", + "depends": ["m6_sn"] + }, + { + "id": "m6_typable_sn", + "label": "typable → SN", + "kind": "paper", + "status": "planned", + "milestone": "M6", + "section": "6", + "file": "", + "depends": ["m6_intersection"] + }, + { + "id": "m6_sn_typable", + "label": "SN → typable", + "kind": "paper", + "status": "planned", + "milestone": "M6", + "section": "6", + "file": "", + "depends": ["m6_typable_sn"] + }, + { + "id": "corollary_6_21_psn", + "label": "Cor 6.21 PSN", + "kind": "paper", + "status": "planned", + "milestone": "M6", + "section": "6", + "file": "", + "depends": ["m6_sn_typable", "theorem_confluence_terms"] + } + ] +} diff --git a/scripts/audit.sh b/scripts/audit.sh new file mode 100755 index 0000000..2c0c386 --- /dev/null +++ b/scripts/audit.sh @@ -0,0 +1,52 @@ +#!/usr/bin/env bash +set -euo pipefail +ROOT="$(cd "$(dirname "$0")/.." && pwd)" +cd "$ROOT" + +if ! command -v rocq >/dev/null 2>&1; then + if command -v opam >/dev/null 2>&1; then + eval "$(opam env --switch=rocq-system --set-switch 2>/dev/null || true)" + fi +fi + +if ! command -v rocq >/dev/null 2>&1; then + echo "rocq not on PATH; run: eval \$(opam env --switch=rocq-system --set-switch)" >&2 + exit 1 +fi + +fail=0 + +echo "== forbidden tokens ==" +while IFS= read -r -d '' f; do + if grep -nE '\b(Admitted|admit|Axiom|Conjecture|native_compute)\b|TODO|FIXME|XXX' "$f"; then + echo "forbidden token in $f" >&2 + fail=1 + fi +done < <(find theory -name '*.v' -print0 2>/dev/null) + +echo "== forbidden Parameter ==" +while IFS= read -r -d '' f; do + if grep -nE '^[[:space:]]*Parameter[[:space:]]' "$f"; then + echo "forbidden Parameter in $f" >&2 + fail=1 + fi +done < <(find theory -name '*.v' -print0 2>/dev/null) + +echo "== Print Assumptions ==" +mkdir -p /tmp/opencode/audit +out="$(rocq compile -o /tmp/opencode/audit/ExecReducer.vo theory/ExecReducer.v 2>&1 || true)" +echo "$out" +if echo "$out" | grep -q "Axioms:"; then + echo "unexpected axioms reported" >&2 + fail=1 +fi +if ! echo "$out" | grep -q "Closed under the global context"; then + echo "no Closed-under-global-context report found" >&2 + fail=1 +fi + +if [ "$fail" -ne 0 ]; then + echo "AUDIT FAIL" + exit 1 +fi +echo "AUDIT OK" diff --git a/scripts/gen_graphs.py b/scripts/gen_graphs.py new file mode 100755 index 0000000..a572dd9 --- /dev/null +++ b/scripts/gen_graphs.py @@ -0,0 +1,180 @@ +#!/usr/bin/env python3 +import json +import os +import subprocess +import sys + +ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +GRAPH_DIR = os.path.join(ROOT, "graphs") +META = os.path.join(GRAPH_DIR, "theorems.json") + +STATUS_FILL = { + "proved": "#d9ead3", + "stated": "#fff2cc", + "planned": "#f3f3f3", + "blocked": "#f4cccc", +} +STATUS_PEN = { + "proved": "#38761d", + "stated": "#b45f06", + "planned": "#777777", + "blocked": "#cc0000", +} +STATUS_STYLE = { + "proved": "filled", + "stated": "filled,dashed", + "planned": "dashed", + "blocked": "filled,bold", +} +INK = "#333333" +RULE_B = "#990000" +RULE_R = "#674ea7" +RULE_G = "#38761d" + + +def q(s): + return '"' + str(s).replace("\\", "\\\\").replace('"', '\\"') + '"' + + +def load(): + with open(META, "r", encoding="utf-8") as f: + return json.load(f) + + +def dependency_dot(data): + nodes = data["nodes"] + by_id = {n["id"]: n for n in nodes} + title = data["paper"]["title"] + " - theorem dependency (" + data["current"] + ")" + lines = [ + "digraph theorem_deps {", + " rankdir=LR;", + " bgcolor=\"white\";", + " node [fontname=Inter, fontsize=10, fontcolor=\"%s\"];" % INK, + " edge [fontname=Inter, fontsize=8, color=\"%s\"];" % INK, + " graph [fontname=Inter, fontsize=12, labelloc=t, label=%s];" % q(title), + ] + for ms in data["milestones"]: + members = [n for n in nodes if n["milestone"] == ms] + if not members: + continue + lines.append(" subgraph cluster_%s {" % ms) + lines.append(" label=%s;" % q(ms)) + lines.append(" style=\"rounded\";") + lines.append(" color=\"#bbbbbb\";") + lines.append(" fontcolor=\"%s\";" % INK) + for n in members: + fill = STATUS_FILL.get(n["status"], "#f3f3f3") + pen = STATUS_PEN.get(n["status"], "#777777") + style = STATUS_STYLE.get(n["status"], "dashed") + tip = n["id"] + if n.get("section"): + tip += " (section " + n["section"] + ")" + if n.get("file"): + tip += " " + n["file"] + tip += " " + data["paper"]["html"] + attrs = [ + "label=%s" % q(n["label"]), + "color=%s" % q(pen), + "fillcolor=%s" % q(fill), + "style=%s" % q(style), + "fontcolor=%s" % q(INK), + "tooltip=%s" % q(tip), + "shape=%s" % ("box" if n["kind"] == "paper" else "ellipse"), + ] + lines.append(" %s [%s];" % (n["id"], ", ".join(attrs))) + lines.append(" }") + for n in nodes: + for d in n.get("depends", []): + if d in by_id: + lines.append(" %s -> %s;" % (d, n["id"])) + lines.append("}") + return "\n".join(lines) + "\n" + + +def rules_dot(): + box = 'shape=box, style="rounded,filled", fillcolor="#f5f5f5", color="%s", fontcolor="%s"' % (INK, INK) + lines = [ + "digraph lambda_sub_cfg {", + " rankdir=TB;", + " bgcolor=\"white\";", + " node [fontname=Inter, fontsize=10];", + " edge [fontname=Inter, fontsize=9, color=\"%s\"];" % INK, + " start [label=\"term\", shape=oval, style=filled, fillcolor=\"#f3f3f3\", color=\"%s\"];" % INK, + " beta [label=\"(lambda x. t) u\", %s];" % box, + " es [label=\"t[x/u]\", %s];" % box, + " pure [label=\"pure term\", shape=oval, style=filled, fillcolor=\"#f3f3f3\", color=\"%s\"];" % INK, + " nf [label=\"normal form\", shape=doublecircle, style=filled, fillcolor=\"#d9ead3\", color=\"%s\"];" % RULE_G, + " start -> beta [label=\"App(Lam,_)\"];", + " start -> es [label=\"ESub\"];", + " start -> pure [label=\"BVar/FVar/Lam\"];", + " beta -> es [label=\"B\", color=\"%s\"];" % RULE_B, + " es -> es [label=\"R (one occurrence)\", color=\"%s\"];" % RULE_R, + " es -> pure [label=\"Gc (x not in fv)\", color=\"%s\"];" % RULE_G, + " pure -> pure [label=\"B under context\", color=\"%s\"];" % RULE_B, + " es -> nf [label=\"R/Gc normalisation\", color=\"%s\"];" % RULE_R, + "}", + ] + return "\n".join(lines) + "\n" + + +def reduction_dot(): + box = 'shape=box, style="filled", fillcolor="#f5f5f5", color="%s", fontcolor="%s"' % (INK, INK) + lines = [ + "digraph reduction_dup {", + " rankdir=LR;", + " bgcolor=\"white\";", + " node [fontname=Inter, fontsize=10];", + " edge [fontname=Inter, fontsize=9, color=\"%s\"];" % INK, + " graph [labelloc=t, fontcolor=\"%s\", label=\"(lambda x. x x) y reduction graph\"];" % INK, + " n0 [label=\"(lambda x. x x) y\", %s];" % box, + " n1 [label=\"(x x)[x/y]\", %s];" % box, + " n2 [label=\"(y x)[x/y]\", %s];" % box, + " n2b [label=\"(x y)[x/y]\", %s];" % box, + " n3 [label=\"(y y)[x/y]\", %s];" % box, + " nf [label=\"y y (normal form)\", shape=doublecircle, style=filled, fillcolor=\"#d9ead3\", color=\"%s\", fontcolor=\"%s\"];" % (RULE_G, INK), + " n0 -> n1 [label=\"B\", color=\"%s\"];" % RULE_B, + " n1 -> n2 [label=\"R\", color=\"%s\"];" % RULE_R, + " n1 -> n2b [label=\"R\", color=\"%s\"];" % RULE_R, + " n2 -> n3 [label=\"R\", color=\"%s\"];" % RULE_R, + " n2b -> n3 [label=\"R\", color=\"%s\"];" % RULE_R, + " n3 -> nf [label=\"Gc\", color=\"%s\"];" % RULE_G, + " {rank=same; n2; n2b;}", + "}", + ] + return "\n".join(lines) + "\n" + + +def run_dot(path): + svg = path[:-4] + ".svg" + png = path[:-4] + ".png" + ok = True + for fmt, out in (("svg", svg), ("png", png)): + r = subprocess.run(["dot", "-T" + fmt, path, "-o", out], capture_output=True, text=True) + if r.returncode != 0: + print(r.stderr, file=sys.stderr) + ok = False + else: + print("wrote", os.path.relpath(out, ROOT)) + return ok + + +def main(): + data = load() + outputs = { + "dependency.dot": dependency_dot(data), + "rules.dot": rules_dot(), + "reduction.dot": reduction_dot(), + } + ok = True + for name, text in outputs.items(): + p = os.path.join(GRAPH_DIR, name) + with open(p, "w", encoding="utf-8") as f: + f.write(text) + print("wrote", os.path.relpath(p, ROOT)) + if not run_dot(p): + ok = False + return 0 if ok else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/theory/ExecReducer.v b/theory/ExecReducer.v new file mode 100644 index 0000000..01cc7cc --- /dev/null +++ b/theory/ExecReducer.v @@ -0,0 +1,272 @@ +From Stdlib Require Import List Bool PeanoNat Lia. +Import ListNotations. + +Definition atom := nat. + +Inductive trm : Type := +| BVar : nat -> trm +| FVar : atom -> trm +| App : trm -> trm -> trm +| Lam : trm -> trm +| ESub : trm -> trm -> trm. + +Fixpoint fvs (t : trm) : list atom := + match t with + | BVar _ => [] + | FVar x => [x] + | App t1 t2 => fvs t1 ++ fvs t2 + | Lam t1 => fvs t1 + | ESub t1 t2 => fvs t1 ++ fvs t2 + end. + +Definition in_fvs (x : atom) (t : trm) : bool := + existsb (Nat.eqb x) (fvs t). + +Fixpoint lift (k : nat) (t : trm) : trm := + match t with + | BVar n => if Nat.ltb n k then BVar n else BVar (S n) + | FVar x => FVar x + | App t1 t2 => App (lift k t1) (lift k t2) + | Lam t1 => Lam (lift (S k) t1) + | ESub t1 t2 => ESub (lift (S k) t1) (lift k t2) + end. + +Fixpoint open_rec (k : nat) (u : trm) (t : trm) : trm := + match t with + | BVar n => if Nat.eqb n k then lift k u else BVar n + | FVar x => FVar x + | App t1 t2 => App (open_rec k u t1) (open_rec k u t2) + | Lam t1 => Lam (open_rec (S k) u t1) + | ESub t1 t2 => ESub (open_rec (S k) u t1) (open_rec k u t2) + end. + +Fixpoint close_rec (x : atom) (k : nat) (t : trm) : trm := + match t with + | BVar n => BVar n + | FVar y => if Nat.eqb y x then BVar k else FVar y + | App t1 t2 => App (close_rec x k t1) (close_rec x k t2) + | Lam t1 => Lam (close_rec x (S k) t1) + | ESub t1 t2 => ESub (close_rec x (S k) t1) (close_rec x k t2) + end. + +Definition subst (x : atom) (u t : trm) : trm := + open_rec 0 u (close_rec x 0 t). + +Fixpoint occurs (n : nat) (t : trm) : bool := + match t with + | BVar m => Nat.eqb m n + | FVar _ => false + | App t1 t2 => occurs n t1 || occurs n t2 + | Lam t1 => occurs (S n) t1 + | ESub t1 t2 => occurs (S n) t1 || occurs n t2 + end. + +Definition occurs0 (t : trm) : bool := occurs 0 t. + +Inductive rule : Type := RB | RGc | RR. + +Definition rule_eqb (r s : rule) : bool := + match r, s with + | RB, RB => true + | RGc, RGc => true + | RR, RR => true + | _, _ => false + end. + +Inductive zctx : Type := +| ZTop : zctx +| ZAppL : zctx -> trm -> zctx +| ZAppR : trm -> zctx -> zctx +| ZLam : zctx -> zctx +| ZESubL : zctx -> trm -> zctx +| ZESubR : trm -> zctx -> zctx. + +Fixpoint zplug (C : zctx) (k : nat) (t : trm) : trm := + match C with + | ZTop => t + | ZAppL C1 u => App (zplug C1 k t) u + | ZAppR u C1 => App u (zplug C1 k t) + | ZLam C1 => Lam (zplug C1 (S k) t) + | ZESubL C1 u => ESub (zplug C1 (S k) t) u + | ZESubR t1 C1 => ESub t1 (zplug C1 k t) + end. + +Fixpoint zplug_lift (C : zctx) (k : nat) (t : trm) : trm := + match C with + | ZTop => lift k t + | ZAppL C1 u => App (zplug_lift C1 k t) u + | ZAppR u C1 => App u (zplug_lift C1 k t) + | ZLam C1 => Lam (zplug_lift C1 (S k) t) + | ZESubL C1 u => ESub (zplug_lift C1 (S k) t) u + | ZESubR t1 C1 => ESub t1 (zplug_lift C1 k t) + end. + +Fixpoint zdecs (t : trm) (k : nat) : list zctx := + match t with + | BVar n => if Nat.eqb n k then [ZTop] else [] + | FVar _ => [] + | App t1 t2 => + map (fun C => ZAppL C t2) (zdecs t1 k) + ++ map (fun C => ZAppR t1 C) (zdecs t2 k) + | Lam t1 => map ZLam (zdecs t1 (S k)) + | ESub t1 t2 => + map (fun C => ZESubL C t2) (zdecs t1 (S k)) + ++ map (fun C => ZESubR t1 C) (zdecs t2 k) + end. + +Definition root_steps (t : trm) : list (rule * trm) := + match t with + | App (Lam body) u => [(RB, ESub body u)] + | ESub body u => + (if occurs0 body then [] else [(RGc, body)]) + ++ map (fun C => (RR, ESub (zplug_lift C 0 u) u)) (zdecs body 0) + | _ => [] + end. + +Inductive ctx : Type := +| GHole : ctx +| GAppL : ctx -> trm -> ctx +| GAppR : trm -> ctx -> ctx +| GLam : ctx -> ctx +| GESubL : ctx -> trm -> ctx +| GESubR : trm -> ctx -> ctx. + +Fixpoint plug (C : ctx) (t : trm) : trm := + match C with + | GHole => t + | GAppL C1 u => App (plug C1 t) u + | GAppR u C1 => App u (plug C1 t) + | GLam C1 => Lam (plug C1 t) + | GESubL C1 u => ESub (plug C1 t) u + | GESubR t1 C1 => ESub t1 (plug C1 t) + end. + +Fixpoint positions (t : trm) : list ctx := + GHole :: + match t with + | BVar _ => [] + | FVar _ => [] + | App t1 t2 => + map (fun C => GAppL C t2) (positions t1) + ++ map (fun C => GAppR t1 C) (positions t2) + | Lam t1 => map GLam (positions t1) + | ESub t1 t2 => + map (fun C => GESubL C t2) (positions t1) + ++ map (fun C => GESubR t1 C) (positions t2) + end. + +Fixpoint at_ctx (C : ctx) (t : trm) : option trm := + match C, t with + | GHole, t => Some t + | GAppL C1 _, App t1 _ => at_ctx C1 t1 + | GAppR _ C2, App _ t2 => at_ctx C2 t2 + | GLam C1, Lam t1 => at_ctx C1 t1 + | GESubL C1 _, ESub t1 _ => at_ctx C1 t1 + | GESubR _ C2, ESub _ t2 => at_ctx C2 t2 + | _, _ => None + end. + +Definition step_at (C : ctx) (t : trm) : list (rule * trm) := + match at_ctx C t with + | None => [] + | Some s => map (fun p => (fst p, plug C (snd p))) (root_steps s) + end. + +Definition steps (t : trm) : list (rule * trm) := + flat_map (fun C => step_at C t) (positions t). + +Definition has_rule (r : rule) (l : list (rule * trm)) : bool := + existsb (fun p => rule_eqb r (fst p)) l. + +Definition count_rule (r : rule) (l : list (rule * trm)) : nat := + length (filter (fun p => rule_eqb r (fst p)) l). + +Definition normal_form (t : trm) : bool := + match steps t with [] => true | _ => false end. + +Definition ex_id : trm := App (Lam (BVar 0)) (FVar 1). +Definition ex_dup : trm := App (Lam (App (BVar 0) (BVar 0))) (FVar 1). +Definition ex_dup_es : trm := ESub (App (BVar 0) (BVar 0)) (FVar 1). +Definition ex_es : trm := ESub (BVar 0) (FVar 1). +Definition ex_gc : trm := ESub (FVar 2) (FVar 1). +Definition ex_nested : trm := ESub (ESub (BVar 0) (FVar 1)) (FVar 2). + +Example ex_id_beta : has_rule RB (steps ex_id) = true. +Proof. reflexivity. Qed. + +Example ex_id_one_step : length (steps ex_id) = 1. +Proof. reflexivity. Qed. + +Example ex_dup_beta : has_rule RB (steps ex_dup) = true. +Proof. reflexivity. Qed. + +Example ex_dup_es_two_R : count_rule RR (steps ex_dup_es) = 2. +Proof. reflexivity. Qed. + +Example ex_dup_es_no_Gc : has_rule RGc (steps ex_dup_es) = false. +Proof. reflexivity. Qed. + +Example ex_es_R : has_rule RR (steps ex_es) = true. +Proof. reflexivity. Qed. + +Example ex_es_no_Gc : has_rule RGc (steps ex_es) = false. +Proof. reflexivity. Qed. + +Example ex_gc_gc : has_rule RGc (steps ex_gc) = true. +Proof. reflexivity. Qed. + +Example ex_gc_no_R : has_rule RR (steps ex_gc) = false. +Proof. reflexivity. Qed. + +Example ex_nested_has_gc : has_rule RGc (steps ex_nested) = true. +Proof. reflexivity. Qed. + +Example ex_id_terminates : normal_form (plug GHole (FVar 5)) = true. +Proof. reflexivity. Qed. + +Example fvs_lam : fvs (Lam (App (BVar 0) (FVar 1))) = [1]. +Proof. reflexivity. Qed. + +Example fvs_es : fvs (ESub (FVar 0) (FVar 1)) = [0; 1]. +Proof. reflexivity. Qed. + +Example occurs0_lam : occurs0 (Lam (BVar 0)) = false. +Proof. reflexivity. Qed. + +Example occurs0_bvar : occurs0 (BVar 0) = true. +Proof. reflexivity. Qed. + +Example open_basic : open_rec 0 (FVar 1) (BVar 0) = FVar 1. +Proof. reflexivity. Qed. + +Example open_under_lam : open_rec 0 (FVar 1) (Lam (BVar 1)) = Lam (FVar 1). +Proof. reflexivity. Qed. + +Example subst_hit : subst 0 (FVar 1) (FVar 0) = FVar 1. +Proof. reflexivity. Qed. + +Example subst_miss : subst 0 (FVar 1) (FVar 2) = FVar 2. +Proof. reflexivity. Qed. + +Example capture_avoid_1 : + subst 0 (FVar 1) (Lam (BVar 0)) = Lam (BVar 0). +Proof. reflexivity. Qed. + +Example capture_avoid_2 : + subst 0 (FVar 1) (Lam (App (BVar 0) (FVar 0))) + = Lam (App (BVar 0) (FVar 1)). +Proof. reflexivity. Qed. + +Example capture_avoid_es : + subst 0 (FVar 1) (ESub (FVar 0) (FVar 2)) + = ESub (FVar 1) (FVar 2). +Proof. reflexivity. Qed. + +Print Assumptions ex_id_beta. +Print Assumptions ex_dup_es_two_R. +Print Assumptions ex_gc_gc. +Print Assumptions ex_nested_has_gc. +Print Assumptions capture_avoid_1. +Print Assumptions capture_avoid_2. +Print Assumptions capture_avoid_es. +Print Assumptions open_under_lam. diff --git a/theory/dune b/theory/dune new file mode 100644 index 0000000..7f43088 --- /dev/null +++ b/theory/dune @@ -0,0 +1,3 @@ +(rocq.theory + (name LambdaSub) + (theories Stdlib))