Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <h2>Functions and propositions</h2> <p>There is a crucial difference between encoding stuff as propositions and functions. Let's take a look at the <code>_+_</code> implemented as a relation on numbers and as a function.</p> <p>Function is trivial, of course:</p> <pre><code>_+_ : (m n : ℕ) → ℕ zero + n = n suc m + n = suc (m + n) </code></pre> <p><code>_+_</code> as a proposition is a ternary relation on numbers. For numbers <code>m</code>, <code>n</code> and <code>o</code>, it should hold precisely when <code>m + n = o</code>:</p> <pre><code>data _+_≡_ : ℕ → ℕ → ℕ → Set where zero : ∀ { n } → zero + n ≡ n suc : ∀ {m n o} → m + n ≡ o → suc m + n ≡ suc o </code></pre> <p>We can for example show that <code>2 + 3 ≡ 5</code>:</p> <pre><code>proof : 2 + 3 ≡ 5 proof = suc (suc zero) </code></pre> <p>Now, functions are more strict about what is allowed: it must pass the termination checker, there must be a unique result, all cases must be covered and so on; in return, they give us computability. Propositions allow redundancy, inconsistency, partial coverage and so on, but to actually show that <code>2 + 3 = 5</code>, the programer must be involved.</p> <p>This is of course a show stopper for your <code>if</code>: you need to be able to compute its first argument!</p> <h2>Is it even?</h2> <p>But there is hope: we can show that your <code>even</code> proposition is actually computable (I should say decidable) for every natural number. How do we show that? By writing a function to decide it.</p> <p>We'll need a negation on propositions:</p> <pre><code>data ⊥ : Set where ¬_ : Set → Set ¬ A = A → ⊥ </code></pre> <p>Next, we'll write down a data type to tell us whether the propositon holds or not:</p> <pre><code>data Dec (P : Set) : Set where yes : P → Dec P no : ¬ P → Dec P </code></pre> <p>And lastly, we'll define what it means for <code>even</code> to be decidable:</p> <pre><code>EvenDecidable : Set EvenDecidable = ∀ n → Dec (even n) </code></pre> <p>This reads: <code>even</code> is decidable if for any natural number <code>n</code> we can show that either <code>even n</code> or <code>¬ (even n)</code>. Let's show that this is indeed true:</p> <pre><code>isEven : EvenDecidable isEven zero = yes _ isEven (suc zero) = no λ () isEven (suc (suc n)) = isEven n </code></pre> <h2>From <code>Dec</code> to <code>Bool</code></h2> <p>Now, we have:</p> <pre><code>data Bool : Set where true false : Bool if_then_else_ : {A : Set} → Bool → A → A → A if true then t else _ = t if false then _ else f = f </code></pre> <p>and a function <code>isEven</code> which returns <code>Dec</code>, not <code>Bool</code>. We can go from <code>Dec</code> to <code>Bool</code> by simply forgetting the proof inside (<code>⌊</code> can be entered via <code>\clL</code>, <code>⌋</code> via <code>\clR</code>):</p> <pre><code>⌊_⌋ : {P : Set} → Dec P → Bool ⌊ yes _ ⌋ = true ⌊ no _ ⌋ = false </code></pre> <p>And finally, we can use <code>isEven</code> in <code>if</code>:</p> <pre><code>if ⌊ isEven n ⌋ then ? else ? </code></pre> <h2>Deriving contradiction</h2> <p>Next, your <code>g</code> function: you require a proof of both <code>even n</code> and <code>even (suc n)</code>. This won't work, because no-one can possibly give both of those. In fact, we can even derive a contradiction using those:</p> <pre><code>bad : ∀ n → even n → even (suc n) → ⊥ bad zero p q = q bad (suc zero) p q = p bad (suc (suc n)) p q = bad n p q </code></pre> <p>However, both</p> <pre><code>bad₂ : ∀ n → even n → even (suc n) → ℕ bad₂ n p q = div (suc n) q bad₃ : ∀ n → even n → even (suc n) → ℕ bad₃ n p q = div n p </code></pre> <p>typecheck just fine, so I am not entirely sure why you have a problem with the second <code>if</code>.</p> <h2>Putting it all together</h2> <p>Now, we are getting to the main part, the <code>odd</code> function. If we know that number is not <code>even</code>, we should be able to show that the successor is <code>even</code>. We'll reuse the negation from before. <code>agda-mode</code> can fill right hand sides with just <code>C-c C-a</code>:</p> <pre><code>odd : ∀ n → ¬ even n → even (suc n) odd zero p = p _ odd (suc zero) p = _ odd (suc (suc n)) p = odd n p </code></pre> <p>Now we have all ingredients to write your <code>g</code> function:</p> <pre><code>g : ℕ → ℕ g n = ? </code></pre> <p>We'll ask whether the number is <code>even</code> using the <code>isEven</code> function:</p> <pre><code>g : ℕ → ℕ g n with isEven n ... | isItEven = ? </code></pre> <p>Now, we'll pattern match on <code>isItEven</code> to find out what the result was:</p> <pre><code>g : ℕ → ℕ g n with isEven n ... | yes e = ? ... | no o = ? </code></pre> <p><code>e</code> is a proof that the number is <code>even</code>, <code>o</code> is a proof that it is not <code>even</code> (it has a type <code>¬ even n</code>). <code>e</code> can be used directly with <code>div</code>, for <code>o</code> we need to use the <code>odd</code> function defined before:</p> <pre><code>g : ℕ → ℕ g n with isEven n ... | yes e = div n e ... | no o = div (suc n) (odd n o) </code></pre> <h2><code>if</code> for <code>Dec</code></h2> <p>You cannot implement the above version with just <code>if</code>, however. <code>Bool</code>eans do not carry any additional information around; they most certainly don't carry the proof we need. We can write a variant of <code>if</code> that works with <code>Dec</code> rather than <code>Bool</code>. This gives us the ability to distribute the relevant proofs to the <code>then</code> and <code>else</code> branches.</p> <pre><code>if-dec_then_else_ : {P A : Set} → Dec P → (P → A) → (¬ P → A) → A if-dec yes p then t else _ = t p if-dec no ¬p then _ else f = f ¬p </code></pre> <p>Notice that both branches are actually functions that take the proof as its first argument.</p> <pre><code>g : ℕ → ℕ g n = if-dec isEven n then (λ e → div n e) else (λ o → div (suc n) (odd n o)) </code></pre> <p>We can even create a fine syntax rule for this <code>if</code>; in this case it's mostly useless, though:</p> <pre><code>if-syntax = if-dec_then_else_ syntax if-syntax dec (λ yup → yupCase) (λ nope → nopeCase) = if-dec dec then[ yup ] yupCase else[ nope ] nopeCase g : ℕ → ℕ g n = if-dec isEven n then[ e ] div n e else[ o ] div (suc n) (odd n o) </code></pre> <h2>What's <code>with</code>?</h2> <p>Now, I noticed that the <code>with</code> construct is mentioned in the later parts of the introduction you linked in the previous question. Here's how it works:</p> <p>Sometimes you need to pattern match on intermediate expressions, such as <code>isEven</code> in the code above. To do that without <code>with</code>, you need to actually write two functions:</p> <pre><code>h₁ : (n : ℕ) → Dec (even n) → ℕ h₁ n (yes e) = div n e h₁ n (no o) = div (suc n) (odd n o) h₂ : ℕ → ℕ h₂ n = h₁ n (isEven n) </code></pre> <p><code>h₂</code> sets up the expression we would like to pattern match on and <code>h₁</code> does the actual pattern matching. Now, pattern matching on intermediate expressions like that is fairly frequent so Agda gives us far more compact notation.</p> <pre><code>h : ℕ → ℕ h n with isEven n h n | yes e = div n e h n | no o = div (suc n) (odd n o) </code></pre> <p>So, <code>with</code> behaves as if it added an extra argument which we can pattern match on. You can even use <code>with</code> on more than one expression at the same time:</p> <pre><code>i : ℕ → ℕ i n with isCool n | isBig n i n | cool | big = ? </code></pre> <p>We can then pattern match on <code>cool</code> and <code>big</code> as if the function had 3 arguments. Now, most of the time the original left hand side stays the same, as the previous functions show (in some cases it can actually be different, but we don't need to deal with that at the moment). For these cases we get a convenient shortcut (especially when the left hand side is long):</p> <pre><code>i : ℕ → ℕ i n with isCool n | isBig n ... | cool | big = ? </code></pre>
    singulars
    1. This table or related slice is empty.
    1. POAgda: how does one obtain a value of a dependent type?
      singulars
      1. PTQuestion
    1. PTAnswer
    1. USVitus
    1. USVitus
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POAgda: how does one obtain a value of a dependent type?
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COThis was a fantastic answer!! Thank you so much for the deep, thoughtful, and dedicated answer. By the way, what are the ...?
      singulars
      1. PO
      1. USJonathan Gallagher
    2. CO@JonathanGallagher: `...` is just a shortcut for left hand side. Take a look at the last two code samples and the paragraph between them: those two functions are identical as far as Agda is concerned.
      singulars
      1. PO
      1. USVitus
    3. COAh. Yes. I noticed that right after I submitted. Thank you.
      singulars
      1. PO
      1. USJonathan Gallagher
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload