[Agda] Symmetry

Fri May 4 18:09:16 CEST 2018

Cool, thanks! -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 4 May 2018 at 13:01, Jacques Carette <carette at mcmaster.ca> wrote:

> I have a Ph.D. student actively looking into deriving various 'free'
> things from theories. Term languages and term orders are included.  No tool
> available yet, but I'm hopeful we'll have something by the fall.
>
> Jacques
>
>
> On 2018-05-04 11:55 AM, Philip Wadler wrote:
>
> Thanks, James. You note the proof of totality has c^2 easy cases, but it
> is no easier than repeating the redundant cases in a proof of determinism.
> Your suggestion fails to simplify the proof, but would help if one had more
> than one proof where one wished to exploit symmetry, or if one already had
> a total order for some other reason. (I expect one could derive a total
> order on reductions from a total order on terms, which would also help.)
>
> Sounds like what Agda needs is a tool for deriving lexicographic orders,
> *including* a proof that the lexicographic order is a total order. Is
> anyone looking at such a tool? I remember Ulf describing how deriving
> supports decidable equality.
>
> Cheers, -- P
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
> On 3 May 2018 at 18:34, James Wood <james.wood.100 at strath.ac.uk> wrote:
>
>> I believe I've done the same sort of thing before by introducing a
>> (constructively) total ordering between the things that should be
>> handled symmetrically. I'm not sure whether it really is helpful, but it
>> might be worth a try. I wrote up a simplified example at [0], which I'll
>> explain the approach of here.
>>
>> First, introduce a relation _≤_ : ∀ {M M′ M″} → (M ⟶ M′) → (M ⟶ M″) →
>> Set, and prove total : ∀ {M M′ M″} → (r0 : M ⟶ M′) (r1 : M ⟶ M″) → r0 ≤
>> r1 ⊎ r1 ≤ r0. The relation _≤_ should roughly be what deriving Ord would
>> give in Haskell, though all of the data in the _⟶_ constructors except
>> inductive positions can be ignored for simplicity. For example, if you
>> wanted this relation to be over List A, the definition could be:
>>
>>   data _≤_ : (xs ys : List A) → Set where
>>     []≤[] : [] ≤ []
>>     []≤∷ : ∀ {x xs} → [] ≤ x ∷ xs
>>     ∷≤∷ : ∀ {x y xs ys} → xs ≤ ys → x ∷ xs ≤ y ∷ ys
>>
>> This does not assume any ordering on A. Notice that this definition will
>> have tr(c) constructors, where c is the number of constructors of the
>> original type (List, _⟶_).
>>
>> Next, prove the lemma det-≤ : ∀ {M M′ M″} (r0 : M ⟶ M′) (r1 : M ⟶ M″) →
>> r0 ≤ r1 → M′ ≡ M″ by induction on the proof of r0 ≤ r1. This will
>> essentially contain only the cases you wanted to write, with no
>> duplicates. From this, the desired result det is proved by cases on
>> total r0 r1, using det-≤ in both cases (and sym in the second case).
>>
>> The bottleneck in this is the proof of total, which requires the full c²
>> cases. However, this should be an easy proof. Wherever the two head
>> constructors differ, C-c C-a should find the solution, and the c-many
>> diagonal cases are by congruence.
>>
>> James
>>
>> [0]: https://gist.github.com/laMudri/8b98b85ce570a09b464c007b1325ca1b
>>
>> On 03/05/18 12:49, Philip Wadler wrote:
>> > Here is a proof that reduction is deterministic:
>> >
>> >     -- Values do not reduce
>> >     Val-⟶ : ∀ {M N} → Value M → ¬ (M ⟶ N)
>> >     Val-⟶ Fun ()
>> >     Val-⟶ Zero ()
>> >     Val-⟶ (Suc VM) (ξ-suc M⟶N)  =  Val-⟶ VM M⟶N
>> >
>> >
>> >     -- Reduction is deterministic
>> >
>> >     det : ∀ {M M′ M″}
>> >       → (M ⟶ M′)
>> >       → (M ⟶ M″)
>> >         ----------
>> >       → M′ ≡ M″
>> >     det (ξ-·₁ L⟶L′) (ξ-·₁ L⟶L″) =  cong₂ _·_ (det L⟶L′ L⟶L″) refl
>> >     det (ξ-·₁ L⟶L′) (ξ-·₂ VL _) = ⊥-elim (Val-⟶ VL L⟶L′)
>> >     det (ξ-·₁ L⟶L′) (β-→ _) = ⊥-elim (Val-⟶ Fun L⟶L′)
>> >     det (ξ-·₂ VL _) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ VL L⟶L″)
>> >     det (ξ-·₂ _ M⟶M′) (ξ-·₂ _ M⟶M″) = cong₂ _·_ refl (det M⟶M′ M⟶M″)
>> >     det (ξ-·₂ _ M⟶M′) (β-→ VM) = ⊥-elim (Val-⟶ VM M⟶M′)
>> >     det (β-→ VM) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ Fun L⟶L″)
>> >     det (β-→ VM) (ξ-·₂ _ M⟶M″) = ⊥-elim (Val-⟶ VM M⟶M″)
>> >     det (β-→ _) (β-→ _) = refl
>> >     det (ξ-suc M⟶M′) (ξ-suc M⟶M″) = cong `suc_ (det M⟶M′ M⟶M″)
>> >     det (ξ-pred M⟶M′) (ξ-pred M⟶M″) = cong `pred_ (det M⟶M′ M⟶M″)
>> >     det (ξ-pred M⟶M′) β-pred-zero = ⊥-elim (Val-⟶ Zero M⟶M′)
>> >     det (ξ-pred M⟶M′) (β-pred-suc VM) = ⊥-elim (Val-⟶ (Suc VM) M⟶M′)
>> >     det β-pred-zero (ξ-pred M⟶M′) = ⊥-elim (Val-⟶ Zero M⟶M′)
>> >     det β-pred-zero β-pred-zero = refl
>> >     det (β-pred-suc VM) (ξ-pred M⟶M′) = ⊥-elim (Val-⟶ (Suc VM) M⟶M′)
>> >     det (β-pred-suc _) (β-pred-suc _) = refl
>> >     det (ξ-if0 L⟶L′) (ξ-if0 L⟶L″) = cong₃ `if0_then_else_ (det L⟶L′
>> >     L⟶L″) refl refl
>> >     det (ξ-if0 L⟶L′) β-if0-zero = ⊥-elim (Val-⟶ Zero L⟶L′)
>> >     det (ξ-if0 L⟶L′) (β-if0-suc VL) = ⊥-elim (Val-⟶ (Suc VL) L⟶L′)
>> >     det β-if0-zero (ξ-if0 L⟶L″) = ⊥-elim (Val-⟶ Zero L⟶L″)
>> >     det β-if0-zero β-if0-zero = refl
>> >     det (β-if0-suc VL) (ξ-if0 L⟶L″) = ⊥-elim (Val-⟶ (Suc VL) L⟶L″)
>> >     det (β-if0-suc _) (β-if0-suc _) = refl
>> >     det (ξ-Y M⟶M′) (ξ-Y M⟶M″) = cong `Y_ (det M⟶M′ M⟶M″)
>> >     det (ξ-Y M⟶M′) (β-Y refl) = ⊥-elim (Val-⟶ Fun M⟶M′)
>> >     det (β-Y refl) (ξ-Y M⟶M″) = ⊥-elim (Val-⟶ Fun M⟶M″)
>> >     det (β-Y refl) (β-Y refl) = refl
>> >
>> >
>> > The proof and all relevant definitions are here:
>> >   https://wenkokke.github.io/sf/Typed
>> >
>> > Almost half the lines in the above proof are redundant, for example
>> >
>> >     det (ξ-·₁ L⟶L′) (ξ-·₂ VL _) = ⊥-elim (Val-⟶ VL L⟶L′)
>> >     det (ξ-·₂ VL _) (ξ-·₁ L⟶L″) = ⊥-elim (Val-⟶ VL L⟶L″)
>> >
>> >
>> > are essentially identical.
>> >
>> > What I would like to do is delete the redundant lines and add
>> >
>> >     det M⟶M′ M⟶M″ = sym (det M⟶M″ M⟶M′)
>> >
>> >
>> > to the bottom of the proof. But, of course, the termination checker
>> > complains.
>> >
>> > How can I rewrite the proof to exploit symmetry? Cheers, -- P
>> >
>> > .   \ Philip Wadler, Professor of Theoretical Computer Science,
>> > .   /\ School of Informatics, University of Edinburgh
>> > .  /  \ and Senior Research Fellow, IOHK
>> > . http://homepages.inf.ed.ac.uk/wadler/
>> >
>> >
>> > The University of Edinburgh is a charitable body, registered in
>> > Scotland, with registration number SC005336.
>> >
>> >
>> >
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>> >
>>
>>
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180504/2f519d5a/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180504/2f519d5a/attachment.ksh>