--- Day changed Wed Aug 30 2017
subttleWhat's the best way to get the union of two AVL ⟨Set⟩? Using conversion to/from list, or is there a good way to use the "naive" `union` for Tree in Data.AVL?30/08 01:57
subttleThank you for any help.30/08 01:58
WilliamHamiltonmietek updates: turns out that the problems I was having with agda mode were caused by an interaction with my old emacs customization. Since I solved that (I'm now able to use agda properly) the proving experience have been a breeze30/08 08:58
WilliamHamiltons/have/has30/08 08:58
WilliamHamiltonI also completed the first few Ilik tutorials, and I have a question of a more principled nature:30/08 08:59
WilliamHamiltonwhen I prove the soundness and completeness for nbe wrt kripke models, why this suffices to convince ourselves of the fact that the language normalizes?30/08 09:00
WilliamHamiltonis kripke semantic so simple that we should be able to understand that correctness by inspection?30/08 09:00
SaizanWilliamHamilton: you have at least proven that equality is decidable, i expect30/08 09:45
SaizanWilliamHamilton: but if you understand "normalizes" in reference to the operational semantics, it really depends on what your theorem statements look like30/08 09:46
mietekWilliamHamilton: earlier, I should’ve referred you to Chapman’s thesis, chapter 4.5, on OPEs, versus assumption/weakening built-in to the derivation datatype, as Ilik does: https://jmchapman.github.io/papers/thesis.pdf30/08 10:12
mietekWilliamHamilton: with regards to your question, it probably fits better in ##dependent30/08 10:13
mietekWilliamHamilton: if we show `nbe : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ⁿᶠ A`, we will have shown that we can come up with a derivation in normal form, for any derivation.30/08 10:13
mietekWilliamHamilton: of course, we could be returning `unit` every time.30/08 10:14
mietekWilliamHamilton: so, the next step is to check that `nbe` works as we expect it to work.30/08 10:14
mietekWilliamHamilton: this is done in Coquand-Dybjer 1997 for combinatory logic, and in Coquand 2002 for STLC.30/08 10:15
mietek(different Coquands)30/08 10:23
WilliamHamiltonsorry guys, I was afk30/08 10:40
WilliamHamiltonthanks Saizan, indeed my question was poorly worded because of some confusion on my part: after your response it became clear that I need to have a notion of equality, and I need to prove Γ ⊢ t = nf(t) : T as Abel does30/08 10:42
WilliamHamiltonyes mietek, so what is missing from Ilik's tutorial was this point, right?30/08 10:43
mietekbasically, except that _=_ should be a convertibility relation30/08 10:43
mietekI have been trying to learn how to prove this30/08 10:43
WilliamHamiltonright, thanks; in the thesis you just linked, what's the difference between the technique he's using (Big step normalization) and normalization by evaluation?30/08 10:44
mietek##dependent30/08 10:45

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!