Add code for Theo Hepburn's Final Year Project#355
Conversation
|
Thanks, @TheoXIII. Thanks for your contribution. It will take a few days for me to be able to review this to conform to TypeTopology. |
|
Dear @TheoXIII and @martinescardo, First, let me apologise for how slow I've been on this. It's been on my to-do list since July and never floated to the top; but I should have found time to prioritise it. I have had a look through the Agda code and it is great, and is compatible with the currently library (I locally rebased it and there were two minor conflicts only). However, Theo, we need to provide a stronger narrative of the work, as currently this is just the formalisation of your dissertation. The dissertation itself, i.e. the narrative of the mathematical work done, is missing, so we need to bring it back.
Finally:
After these three actions have been done -- and as I say I'm happy to support @TheoXIII with this -- I think we can pass this to @martinescardo for a final review. Best, |
|
Thanks. But there is a lot of checking needed to make sure the many files comply to TypeTopology formatting requirements. This needs to be done (there are many non-compliancies). |
|
Sure — is there a ratified list of rules/guidelines we should be complying with? EDIT: I found this list. I'll review Theo's code with this in mind, and we will work on the narrative together from mid-January. |
|
Also we have a requirement to restrict ourselves to "Spartan MLTT" as much as possible, and, when we don't, say so explicitly. |
tnttodda
left a comment
tnttodda
left a comment
There was a problem hiding this comment.
Theo, once again thank you for all your hard work. Looking forward to meeting online soon to discuss the following review.
For this review, I followed the guidance in CONTRIBUTIONS.md as discussed above.
Contribution directory appropriately organised?
Yes, but we may rename TGH to something else.
Contribution has an index?
Yes.
Indentation is a single space throughout?
Mostly, but not always, see Correction 1 below, but some are solved by Correction 3.
Universe notation used correctly throughout?
Yes.
Equals symbol used correctly throughout?
Yes.
Each module has an appropriate preamble?
Yes.
Line length never exceeds 80 characters?
Yes.
Casing convention followed correctly throughout?
Yes.
All files are .lagda files with code blocks?
Yes.
All code blocks have correct spacing after the start and before the end?
Yes.
Comments and discussions are in files?
No, but see my above comment on this issue for that.
All modules use flags —safe and —without-K?
Yes.
Sigma types used correctly throughout?
Yes, though it might be worth using notation such as ((t , _) : Σ t ꞉ ℕ , Thunk t (List ℕ)) instead of (x : Σ t ꞉ ℕ , Thunk t (List ℕ)) so that you can write t instead of pr_1 x (see for example thunk-if-lemma). See Correction 2 below.
Keyword ‘with’ avoided?
Yes.
Imports sorted alphabetically in the index file?
Yes.
Multiline type signatures broken correctly?
Not always, see Correction 3 below — i.e. check that symbols (such as arrows, etc.) line up with symbols (such as colons, definitional equals, etc.) above and below. Also check that each arrow starts a new line, as is standard.
SpartanMLTT used throughout?
Yes. But one more comment: throughout, you use pr_1 for various purposes to extract time information, the first element of lists, etc. We should see whether we should create some functions that make it clear what these pr_1’s are doing. For example, you have a function called ‘get-time = pr_1’ for extracting time information; so functions similar to this throughout would be great.
Corrections List
Correction 1: Single space indenting
1.1 ComplexityDefinitionsResults.lagda
1.1.1 time-independent-of-list-values
1.1.2 adding-times-lemma
1.1.3 thunk-if-lemma
1.2 Language.lagda
1.2.1 thunk-type
Correction 2: Sigma type patterns
2.1 ComplexityDefinitionsResults.lagda
2.1.1 thunk-if-lemma
2.1.2 adding-times-lemma
2.1.3 adding-times-lemma-l-n-l
2.2 HeadExample.lagda
2.2.1 head-list-value-independent-eager
2.2.2 nat-function-lemma
2.2.3 eager-head-not-constant-time-lemma
2.2.4 eager-head-linear-time-big-o
… (at this point I think you get the idea!)
Correction 3: Multiline type signatures
3.0 BigO.lagda
3.0.1 big-o
3.1 ComplexityDefinitionsResults.lagda
3.1.1 call-intermediate-l
3.1.2 time-independent-of-list-values
3.1.3 time-independent-of-list-values-n
3.1.4 is-linear-time
3.1.5 is-linear-time-n
3.1.6 is-polytime-to-polybig-o
3.1.7 thunk-if-lemma
3.1.8 adding-times-lemma
3.1.9 adding-times-lemma-l-n-l
3.2 HeadExample.lagda
3.2.1 head-correctness
3.2.2 head-time-value-env-independent-lazy
3.2.3 head-list-value-independent-lazy
3.2.4 lazy-head-constant-time
3.2.5 head-list-value-independent-eager
3.2.6 eager-head-not-constant-time-lemma
3.2.7 eager-head-not-constant-time
3.2.8 eager-head-linear-time-big-o
3.2.9 eager-head-linear-time
3.3 InsertionSortCorrectness.lagda
3.3.1 call-intermediate-l-n
3.3.2 concat-env-lemma
3.3.3 concat-correctness
3.3.4 subtract-env-lemma
3.3.5 subtract-correctness
3.3.6 ℕ-subtract-lemma-I
… (at this point I think you get the idea!)
Correction 4: Make sure arguments to multi-variable functions or records are correctly indented for readability
4.1 ComplexityDefinitionsResults.lagda
4.1.1 is-linear-time
4.1.2 is-linear-time-n
4.1.3 is-polytime-to-polybig-o
4.2 HeadExample.lagda
4.2.1 lazy-head-constant-time
4.2.2 head-list-value-independent-eager
4.2.3 eager-head-not-constant-time-lemma
4.2.4 eager-head-not-constant-time
4.2.5 eager-head-linear-time-big-o
4.2.6 eager-head-linear-time'
4.3 InsertionSortCorrectness.lagda (see comment on file)
4.3.1 concat-correctness
4.3.2 subtract-env-lemma
… (at this point I think you get the idea!)
Correction 5: Equational reasoning readability
5.1 ComplexityDefinitionsResults.lagda
5.1.1 adding-times-lemma-l-n-l (rename from 5.1.3)
5.2 HeadExample.lagda
5.2.1 head-time-value-env-independent-lazy
5.2.3 eager-head-env-lemma-II
5.2.4 head-list-value-independent-eager
5.3 InsertionSortCorrectness.lagda
5.3.1 concat-correctness
5.3.2 subtract-correctness
5.3.3 ℕ-subtract-lemma-I
… (at this point I think you get the idea!)
Other comments:
ComplexityDefinitionsResults.lagda
is-polytime-to-polybig-o — Doesn’t the sigmatype want to be replaced with is-linear-time-n?
thunk-if-lemma — I suggest putting the <= on the following line, for readability
InsertionSortCorrectness.lagda
sort-env-lemma — I think it’s tricky to read what’s going on in this function and the ones following it in this file; we can discuss these verbally.
LastTimeListValueIndependent.lagda
recursive-call-comp-same-env — I feel here and throughout, we can remove excessive brackets when we have multiple √ constructors (I tried this and the file type checks fine)
recursive-call-list-value-independent — I think it’s tricky to read what’s going on in this function and the ones following it in this file; we can discuss these verbally.
NP.lagda
_∈NP — It’s hard to see the scoping of the different dependent types here. Make sure to start each on a new line and use indentation so readers can follow the scoping clearly.
P⊆NP — Please replace ‘Pi’ and ‘Sigma’ with the usual notation in this library (i.e. Π n ꞉ ℕ , etc.)
P.lagda
Please replace ‘Pi’ and ‘Sigma’ with the usual notation in this library (i.e. Π n ꞉ ℕ , etc.)
PrototypeLanguage.lagda
is-even-time — Tricky to read what’s going on in this function; we can discuss this verbally.
Thunk.lagda
>>= - -> should be →
| open import Naturals.Order renaming (_≤ℕ_ to _≤_) | ||
|
|
||
| data _∈O[_] (f : ℕ → ℕ) (g : ℕ → ℕ) : 𝓤₀ ̇ where | ||
| big-o : Σ c ꞉ ℕ , Σ N₀ ꞉ ℕ , Π N ꞉ ℕ , (N₀ ≤ N → f N ≤ c * (g N)) |
| gen-naive-list zero = [] | ||
| gen-naive-list (succ n) = 0 ∷ gen-naive-list n | ||
|
|
||
| call-intermediate-l : {σ : LType} {n : ℕ} {Γ : Ctx n} → (env : Envᵢ Γ) |
| ＝ pr₁ (call-intermediate-l env program strategy l₂) | ||
| time-independent-of-list-values env (inr refl) strategy program | ||
| = (l₁ l₂ : List ℕ) → (length l₁ ＝ length l₂) | ||
| → pr₁ (call-intermediate-l env program strategy l₁) |
| → 𝓤₀ ̇ | ||
| time-independent-of-list-values-n env (inl refl) strategy program | ||
| = (l₁ l₂ : List ℕ) → (length l₁ ＝ length l₂) → (n₁ n₂ : ℕ) | ||
| → pr₁ (pr₁ (pr₁ (env [ program ]ᵢ strategy) (thunk-type l₁)) (thunk-type n₁)) |
| ＝ pr₁ (pr₁ (pr₁ (env [ program ]ᵢ strategy) (thunk-type l₂)) (thunk-type n₂)) | ||
| time-independent-of-list-values-n env (inr refl) strategy program | ||
| = (l₁ l₂ : List ℕ) → (length l₁ ＝ length l₂) → (n₁ n₂ : ℕ) | ||
| → pr₁ (pr₁ (pr₁ (env [ program ]ᵢ strategy) (thunk-type l₁)) (thunk-type n₁)) |
| Π l ꞉ List Bool , Σ c ꞉ List Bool , polynomial-length l c k C | ||
| × ((env : Env Γ) → | ||
| (to-decision-verifier env program c l ＝ decision l)) | ||
| × (verifier-polytime program)) |
There was a problem hiding this comment.
It’s hard to see the scoping of the different dependent types here. Make sure to start each on a new line and use indentation so readers can follow the scoping clearly.
| (transport (_≤ length c + length l) (zero-left-neutral (length l)) | ||
| (≤-n-monotone-right 0 (length c) (length l) ⋆)))) | ||
|
|
||
| f : Pi (List ℕ) |
There was a problem hiding this comment.
Please replace ‘Pi’ and ‘Sigma’ with the usual notation in this library (i.e. Π n ꞉ ℕ , etc.)
| (not' ∙ (lam list program ∙ var 𝟎)) | ||
| timing' (k , C , N₀ , f) = k , C + 5 , succ N₀ , f' | ||
| where | ||
| f' : Pi (List ℕ) |
There was a problem hiding this comment.
Please replace ‘Pi’ and ‘Sigma’ with the usual notation in this library (i.e. Π n ꞉ ℕ , etc.)
| γ₂ zero le = refl | ||
| γ₂ (succ zero) le = refl | ||
|
|
||
| γ₃ : (n : ℕ) → force (pr₂ (thunk-if (nat-recᵢ {1} {nat ∷ []} |
There was a problem hiding this comment.
Tricky to read what’s going on in this function; we can discuss this verbally.
| force (√ x) = force x | ||
|
|
||
| _>>=_ : {n₁ n₂ : ℕ} {X Y : 𝓤₀ ̇} | ||
| -> Thunk n₁ X → (X → Thunk n₂ Y) → Thunk (n₂ + n₁) Y |
Hi Ayberk, don't worry, I haven't forgotten this. I've just been busy recently so I'm still trying to find time to do this. |
@TheoXIII Great, no worries. There is no hurry. Just wanted to make sure that it’s not been forgotten. |
4 participants
As requested by Todd and Vincent, this pull request will add the code for my Final Year Project, "Proving time complexity of algorithms and formalising complexity classes in Agda", where I formalise the concept of time complexity, define a simple Lambda calculus-like language, prove the time complexity of some programs in this language, and formalise the complexity classes P and NP. I have also contributed some additional proofs that I wrote about natural number ordering and exponentiation to Naturals.Order and Naturals.Multiplication.