--- Day changed Wed Aug 30 2017 | ||

subttle | What'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 |
---|---|---|

subttle | Thank you for any help. | 30/08 01:58 |

WilliamHamilton | mietek 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 breeze | 30/08 08:58 |

WilliamHamilton | s/have/has | 30/08 08:58 |

WilliamHamilton | I also completed the first few Ilik tutorials, and I have a question of a more principled nature: | 30/08 08:59 |

WilliamHamilton | when 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 |

WilliamHamilton | is kripke semantic so simple that we should be able to understand that correctness by inspection? | 30/08 09:00 |

Saizan | WilliamHamilton: you have at least proven that equality is decidable, i expect | 30/08 09:45 |

Saizan | WilliamHamilton: but if you understand "normalizes" in reference to the operational semantics, it really depends on what your theorem statements look like | 30/08 09:46 |

mietek | WilliamHamilton: 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.pdf | 30/08 10:12 |

mietek | WilliamHamilton: with regards to your question, it probably fits better in ##dependent | 30/08 10:13 |

mietek | WilliamHamilton: 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 |

mietek | WilliamHamilton: of course, we could be returning `unit` every time. | 30/08 10:14 |

mietek | WilliamHamilton: so, the next step is to check that `nbe` works as we expect it to work. | 30/08 10:14 |

mietek | WilliamHamilton: 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 |

WilliamHamilton | sorry guys, I was afk | 30/08 10:40 |

WilliamHamilton | thanks 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 does | 30/08 10:42 |

WilliamHamilton | yes mietek, so what is missing from Ilik's tutorial was this point, right? | 30/08 10:43 |

mietek | basically, except that _=_ should be a convertibility relation | 30/08 10:43 |

mietek | I have been trying to learn how to prove this | 30/08 10:43 |

WilliamHamilton | right, 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 | ##dependent | 30/08 10:45 |

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