[Agda] Re: Associativity for free!

[Alan Jeffrey]

I'll have a look at it, thanks for the pointer!

I'm going to be needing the general form of substitution later (in stuff 
I've not committed yet, which does normalization by evaluation). That's 
not to say I couldn't derive the general form from substitution and 
weakening, but I think it's swings and roundabouts.

A.

On 11/02/2011 12:46 PM, Andreas Abel wrote:
> Hi Alan,
>
> you might be interested in a trick how to fuse weakening and
> substitution into a single operation.  I have done this for
> non-wellscoped de Bruijn terms in Agda:
>
>     http://www2.tcs.ifi.lmu.de/~abel/ParallelSubstitution.agda
>
> but Thorsten and Conor deserve the credit for it (pointers in the .agda
> file).
>
> Looking at your code I wonder whether substitution (substn+) could not
> be a bit less general, since N remains in the same context always.
> Usually I prove the substitution lemma like this:
>
>     Gamma, x : T, Delta |- M : U
>     Gamma               |- N : T
>     ----------------------------
>     Gamma, Delta   |- M[N/x] : U
>
> Your statement has a more general context form for N, but I wonder
> whether this is necessary.
>
> Cheers,
> Andreas
>
> On 11/2/11 5:26 PM, Alan Jeffrey wrote:
>> Hi everyone,
>>
>> My original motivation for "associativity for free" was properties about
>> lambda-calculi. I've now worked through some of the details, and here is
>> the syntax of the simply-typed lambda-calculus:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>>
>>
>> The interesting thing is weakening, with type:
>>
>> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>>
>> and (news just in!) weakening commutes with itself (up to propositional
>> equality):
>>
>> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>>
>> Note that you can't even state this property without associativity on
>> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
>> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>>
>> The proof makes use of a list-membership type, defined in:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>>
>>
>> It satisfies weakening on the left and right:
>>
>> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>>
>> and moreover has left and right units and associativity properties, all
>> up to beta-equivalence (that is, all these properties have proof refl):
>>
>> (a∈as ≪ []) ≡ a∈as
>> ([] ≫ a∈as) ≡ a∈as
>> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>>
>> Under the hood, this is implemented in terms of difference naturals
>> (that is an implementation of ℕ where + and ♯0 form a monoid up to
>> beta-equivalence), and an implementation of difference lists such that
>> the length function is a monoid homomorphism up to beta-equivalence:
>>
>> (len (as ++ bs) ≡ (len as + len bs))
>> (len [] ≡ ♯0)
>>
>> With all that in place, the proof of weakening is pretty
>> straightforward. The only case which requires any work is variables, and
>> a typical case is:
>>
>> begin
>> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>> ∎
>>
>> I don't really want to think about what this proof would look like with
>> all the associativity wiring made explicit.
>>
>> There is still a bit of annoying associativity left, because I can't see
>> how to get coproducts to associate on the nose, so there's lots of gore
>> needed to define a case function:
>>
>> data Case {A} a (as bs : List A) : Set where
>> inj₁ : (a∈as : a ∈ as) → Case a as bs
>> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>>
>> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>>
>> and then prove that it satisfies associativity (up to propositional
>> equality, not beta-equivalence).
>>
>> A.
>>
>> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>>> Hi everyone,
>>>
>>> A quick note about a trick for representing lists (or any other monoid)
>>> up to associativity. Am I reinventing a wheel here?
>>>
>>> I've been doing some mucking around recently with proofs about
>>> lambda-calculi and was hitting annoying problems with associativity
>>> on lists. A prototypical example is:
>>>
>>> weakening : ∀ {A a} (as bs cs : List A) →
>>> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>>
>>> It's easy to prove that ++ is associative, but making use of that fact
>>> is rather painful, as there's lots of manual wiring with subst and cong,
>>> for example:
>>>
>>> weaken2 : ∀ {A a} (as bs cs ds : List A) →
>>> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>>> weaken2 {A} {a} as bs cs ds a∈es =
>>> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>>> (weakening (as ++ bs) cs ds
>>> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>>
>>> This gets tiresome pretty rapidly. Oh if only there were a data
>>> structure which represented lists, but for which ++ was associative up
>>> to beta reduction... Oh look there already is one, it's called
>>> difference lists. Quoting the standard library:
>>>
>>> DiffList : Set → Set
>>> DiffList a = List a → List a
>>>
>>> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>>> xs ++ ys = λ k → xs (ys k)
>>>
>>> Unfortunately, difference lists are not isomorphic to lists: there's a
>>> lot more functions on lists than just concatenation functions. This
>>> causes headaches (e.g. writing inductive functions on difference lists).
>>>
>>> A first shot at fixing this is to write a data structure for those
>>> difference lists which are concatenations:
>>>
>>> record Seq (A : Set) : Set where
>>> constructor seq
>>> field
>>> list : List A
>>> fun : List A → List A
>>> ok : fun ≡ _++_ list -- Broken
>>>
>>> It's pretty straightforward to define the monoidal structure for Seq:
>>>
>>> ε : ∀ {A} → Seq A
>>> ε = seq [] id refl
>>>
>>> _+_ : ∀ {A} → Seq A → Seq A → Seq A
>>> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>>
>>> Unfortunately, we're back to square one again, because + is only
>>> associative up to propositional equality, not beta reduction. This time,
>>> it's the ok field that gets in the way. So we can fix that, and just
>>> make the ok field irrelevant, that is:
>>>
>>> record Seq (A : Set) : Set where
>>> constructor seq
>>> field
>>> list : List A
>>> fun : List A → List A
>>> .ok : fun ≡ _++_ list -- Fixed
>>>
>>> open Seq public renaming (list to [_])
>>>
>>> Hooray, + is now associative up to beta reduction:
>>>
>>> +-assoc : ∀ {A} (as bs cs : Seq A) →
>>> ((as + bs) + cs) ≡ (as + (bs + cs))
>>> +-assoc as bs cs = refl
>>>
>>> Moreover, given (http://thread.gmane.org/gmane.comp.lang.agda/3034):
>>>
>>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>>
>>> we can define:
>>>
>>> data Case {A : Set} : Seq A → Set where
>>> [] : Case ε
>>> _∷_ : ∀ a as → Case (a ◁ as)
>>>
>>> case : ∀ {A} (as : Seq A) → Case as
>>>
>>> and this gives us recursive functions over Seq (which somewhat to my
>>> surprise actually get past the termination checker), for example:
>>>
>>> ids : ∀ {A} → Seq A → Seq A
>>> ids as with case as
>>> ids .(a ◁ as) | a ∷ as = a ◁ ids as
>>> ids .ε | [] = ε
>>>
>>> For example, we can now define weakening:
>>>
>>> weakening : ∀ {A a} (as bs cs : Seq A) →
>>> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>>
>>> and use it up to associativity without worrying hand-coded wiring:
>>>
>>> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>>> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>>> weaken2 as bs = weakening (as + bs)
>>>
>>> Hooray, cake! Eating it!
>>>
>>> I suspect this trick works for most any monoid, so you can do
>>> associativity on naturals, vectors, partial orders with join, etc. etc.
>>>
>>> The idea of using difference lists to represent lists is standard, but
>>> as far as I know, this use of irrelevant equalities to get structural
>>> recursion is new. Anyone know of any prior art?
>>>
>>> A.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>