Complexity and csp definitions (and theorems... soon) #69
Conversation
| ∣C∣ -- # of constraints (resp.) | ||
| : ℕ | ||
| 𝐶 : Fin ∣C∣ → Constraint{χ} ∣V∣ ∣D∣ | ||
| record Constraint (var : Type ν)(dom : Type δ){ρ : Level} : Type (lsuc (ι ⊔ ν ⊔ δ ⊔ ρ)) where |
There was a problem hiding this comment.
Isn't the level that you want (lsuc ι) ⊔ ν ⊔ δ ⊔ (lsuc ρ) ? This is lower (in general). The nice thing about parameters is that they don't cause level creep.
There was a problem hiding this comment.
Correct. How could you possibly have noticed that?!
| Some of the informal (i.e., non-agda) material in this module is similar to that presented in | ||
| \begin{code} | ||
|
|
||
| record CSPInstance (var : Type ν)(dom : Type δ){ρ : Level} : Type (lsuc (ι ⊔ ν ⊔ δ ⊔ ρ)) where |
There was a problem hiding this comment.
This seems oddly formed to me - shouldn't the Constraint be a parameter?
There was a problem hiding this comment.
Well, there's not a single constraint (though you could view it as such). Rather, there is a tuple of contraints, so I use arity to represent the "number" of constraints, and then the constraints are modeled as a function from arity to the Constraint type. Does it still seem odd to you? Perhaps it would have been easier to comprehend if I had called the arity field ∣constraints∣ or something similar? (and then rename the cs field constraints...?)
There was a problem hiding this comment.
I think I was not precise. Isn't a CSPInstance supposed to be an instance of a CSP? In other words, it should be parametrized by a single "problem". The definition used here only have a very diffuse 'problem' that it depends on, quite indirectly.
|
|
||
| record Constraint (∣V∣ ∣D∣ : ℕ) : Type (lsuc (χ ⊔ ρ)) where | ||
| field | ||
| scope : Fin ∣V∣ → Type χ -- a subset of Fin ∣V∣ |
There was a problem hiding this comment.
This seems overly general. There is little point in having witnesses to whether something is in scope. You might as well use Bool instead. And then Vec (Fin |V|) Bool might be easier?
There was a problem hiding this comment.
Very good point. I want to make the FiniteCSP module very special and easy to use, so I'll try the Vec approach you suggest. (That's actually what I started with, but thought it was maybe too special... but probably you're right.)
There was a problem hiding this comment.
Because Fin |V| has decidable equality (and is finite!), you gain very little from having scope be so very general. You may as well have other things also have decidable equality.
a very modest start