38 lines
1.9 KiB
Markdown
38 lines
1.9 KiB
Markdown
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 graphs are drawn in black and white and split by milestone. Every edge runs from a dependency to the result that uses it. A box is a result named after a paper statement, an ellipse is a supporting result, and a dashed box labelled with a milestone is a result defined in another diagram. The overview gives the shape of the whole development:
|
|
|
|
<p align="center"><img src="graphs/dependency-overview.svg?v=black-white" alt="Theorem dependency by milestone"></p>
|
|
|
|
The details are then one diagram per milestone:
|
|
|
|
### M1, binding and reduction
|
|
|
|
<p align="center"><img src="graphs/dependency-M1.svg?v=black-white" alt="M1 dependencies"></p>
|
|
|
|
### M2, metatheory and checks
|
|
|
|
<p align="center"><img src="graphs/dependency-M2.svg?v=black-white" alt="M2 dependencies"></p>
|
|
|
|
### M3, subsystem
|
|
|
|
<p align="center"><img src="graphs/dependency-M3.svg?v=black-white" alt="M3 dependencies"></p>
|
|
|
|
### M4, parallel reduction
|
|
|
|
<p align="center"><img src="graphs/dependency-M4.svg?v=black-white" alt="M4 dependencies"></p>
|
|
|
|
### M5, metaterms and the named calculus
|
|
|
|
<p align="center"><img src="graphs/dependency-M5.svg?v=black-white" alt="M5 dependencies"></p>
|
|
|
|
The rule sketch gives the transition system generated by the rules B and Gc and R:
|
|
|
|
<p align="center"><img src="graphs/rules.svg?v=black-white" alt="Reduction rules"></p>
|
|
|
|
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:
|
|
|
|
<p align="center"><img src="graphs/reduction.svg?v=black-white" alt="Reduction graph of the duplicating identity"></p>
|