Hot answers tagged

7

ℕ→ℕ-undecidable is not provable in Agda. If we postulate the law of excluded middle (LEM), it follows that equality on every set is decidable, contradicting ℕ→ℕ-undecidable. Since Agda is consistent with LEM, it follows that ℕ→ℕ-undecidable is not provable in base Agda. This holds the same for cubical and vanilla Agda.


5

The following explanation lacks mathematicial precision but should explain what is going on. A GADT is a special case of a recursive type. A recursive type $T$ is a solution of a type equation of the form $$T = \Phi(T).$$ (If this is not clear, please ask.) Sometimes $\Phi$ depends on a parameter $p : P$ of some given type $P$, so we have a parameterized ...


4

First, let's desugar the withs. First definition: wa''-aux : ∀ m n -> n + m ≡ m + n -> wa (m + n) ≡ wa (n + m) wa''-aux m n refl = ? -- cannot unify n + m with m + n wa'' : ∀ m n -> wa (m + n) ≡ wa (n + m) wa'' m n = wa''-aux m n (comm n m) Second definition: wa''-aux : ∀ m n w -> w ≡ m + n -> wa (m + n) ≡ wa w wa''-aux m n .(m + n) refl ...


4

The definition is not correct. It states that a machine is polynomial time (the field poly in poly-time-machine) when its running time is below the exponential function $n \mapsto 2^n$ (the definition is-poly). This would allow, for example, a running time $n \mapsto 1.5^n$, which isn not poly-time according to the accepted definition.


3

Yes and no. The obvious difference is that indexed types are able to vary in the result type of each constructor. So you can do: data T : ℕ → Set where t : T 5 You can do this with a parameterized type by taking an argument: data T (n : ℕ) : Set where t : n ≡ 5 → T n But ≡ is itself an indexed type, so you need something indexed at the bottom (≡ can ...


3

Axiom K is related to "Uniqueness of Identity Proofs", which says is that any two proofs of equality are themselves equal to each other (i.e. are both Refl). Agda doesn't include K as an axiom, but it (and UIP) can be proved as a theorem using Agda's dependent pattern matching. Axiom K is inconsistent with homotopy type theory, where the univalence axiom ...


2

The only way to prove ∥ X ∥ is to prove X (unless you admit some other axiom). So, assuming P is a proposition, there is no way to prove ∥ ((A) ⊎ (¬ A)) ∥ if you cannot prove ((A) ⊎ (¬ A)). It is not a correct intuition that undecidable propositions are either true or false, just we do not know about it. A formal system S with an undecidable proposition P ...


2

Many total languages, including Agda and Coq, allow you to define coinductive data types. These model infinite objects, like infinite lists. Obviously, a function producing an infinite list cannot terminate. However, it must, in a total language, be productive. This means that any finite prefix of the produced infinite list can be computed in finite time. ...


Only top voted, non community-wiki answers of a minimum length are eligible