[Agda] How can we define a type of symmetric binary operations in Agda ?

Conor McBride conor at strictlypositive.org
Wed May 6 10:21:37 CEST 2015 

On 5 May 2015, at 16:08, Sergey Kirgizov <sergey.kirgizov at u-bourgogne.fr> wrote:

> On Tue, May 05, 2015 at 10:35:00AM +0100, Conor McBride wrote:
>> data Nat : Set where
>> ze : Nat
>> su : Nat -> Nat
>> 
>> symIter : {X : Set} -> (Nat -> X) -> (X -> X) -> Nat -> Nat -> X
>> symIter zen more ze          n  = zen n
>> symIter zen more m          ze  = zen m
>> symIter zen more (su m) (su n)  = more (symIter zen more m n)
>> 
>> First, show that
>> 
>> symIter zen more
>> 
>> is always commutative.
> 
> Indeed  "symIter"  is  a  beautiful  solution  for  defining  symetric
> operations over finite  and denumerable sets.
> 
> Do I understand correctly that it will work only with finite and denumerable sets?

"Propose to an Englishman any principle, or any instrument, however admirable, and you will observe that the whole effort of the English mind is directed to find a difficulty, a defect, or an impossibility in it. If you speak to him of a machine for peeling a potato, he will pronounce it impossible: if you peel a potato with it before his eyes, he will declare it useless, because it will not slice a pineapple. Impart the same principle or show the same machine to an American or to one of our Colonists, and you will observe that the whole effort of his mind is to find some new application of the principle, some new use for the instrument." C. Babbage

> Imaginde, for example that we have defined Real numbers in Agda.
> Than, we cannot directly use symIter in order to define x:Real + y:Real.
> 
> _+_ : Real → Real → Real
> _+_ = symIter ? ??
> 
> Can we write something like symIter but without using Nat ?

The essence of the situation is that any pair of bits are either equal (to a bit you can see) or different (but you can't see which way round they are). I haven't constructed the following generalisation, but I know what I'd try: (1) figure out how to jack that up structurally: consider how to build a symmetric case analysis for a universe closed under Booleans and Sigma; (2) throw in a placeholder for substructures and develop the symmetric recursor.

Now, very few functions involving real numbers exist, but functions from *representations* of real numbers do exist, so the question is how to define symmetric operations on those representations. E.g., if reals are streams, you can turn a pair of streams into a pair of head-and-tail pairs, and then you can do symmetric case analysis on the heads, and then what?

The message is not that Nat has a specially good behaviour when it comes to symmetry, but that symmetric ways of looking exist more broadly. Indeed the min-and-diff observation generalises to an enhanced equality test which gives you that every pair of values (of whatever datatype) either coincide or have a leftmost discrepancy: that's exactly what I'd expect to establish for my Bool and Sigma universe.

Oh, and yes, for + and *, the key is not to separate them.

dddddD
ccccCd
bbbBcd
aaAbcd

When computing 6*4, it's very useful to know 5*3 and 5+3.

This whole business would work a bunch better with proper quotients (which would allow us to derive symmetric induction principles), but we can get quite some way without them.

All the best

Conor

> 
> Best
> Sergey
> 
>> 
>> Then define max, min, addition and multiplication by instantiating zen and
>> more appropriately.
>> 
>> The key to not seeing more than you should is to change your means of
>> looking.
>> 
>> All the best
>> 
>> Conor
>> 
>> 
>>>> If we had quotient types, one could easily make an "unordered pair"
>>>> type, and make unary relations over that.
>>>> 
>>>> Are there any useful tricks to do something similar in Agda?
>>>> 
>>>> On May 1, 2015 3:07 PM, "Andreas Abel" <abela at chalmers.se
>>>> <mailto:abela at chalmers.se>> wrote:
>>>> 
>>>>  You can create a record with two fields, one is your binary
>>>>  operation, the other the proof of symmetry.
>>>> 
>>>>  record SymBinOp : Set where
>>>>     field
>>>>       _⊙_ : BinaryOperation
>>>>       proof-of-symmetry : ∀ x y → x ⊙ y == y ⊙ x
>>>> 
>>>>  That's it!
>>>> 
>>>>  On 30.04.2015 17:35, Sergey Kirgizov wrote:
>>>> 
>>>>      Hello,
>>>> 
>>>>      I don't  understand how  we can  define in Agda  a type  of
>>>>      "Symmetric
>>>>      Binary Relation". Can you help me?
>>>>      Imagine I have something like:
>>>> 
>>>>      =======================================================
>>>> 
>>>>      {-
>>>>          At first we reaname  Set
>>>> 
>>>>      {-
>>>>          First, we define a polymorphic idenity
>>>>      -}
>>>>      data _==_ {A : 𝓤} (a : A) : A → 𝓤 where
>>>>          definition-of-idenity : a == a
>>>>      infix 30 _==_
>>>> 
>>>>      {-
>>>>         Next we define the finite set Ω = {A,B,C}
>>>>      -}
>>>>      data Ω : 𝓤 where
>>>>          A B C : Ω
>>>> 
>>>>      {-
>>>>         We add a type "Binary operation"
>>>>      -}
>>>>      BinaryOperation = Ω → Ω → Ω
>>>> 
>>>>      {-
>>>>         I can actually define an example of Binary operation.
>>>>      -}
>>>>      _⊙_ : BinaryOperation
>>>>      x ⊙ x' = A
>>>>      infix 40 _⊙_
>>>> 
>>>>      {-
>>>>         And then I can proove that ⊙ is Symmetric
>>>>      -}
>>>>      proof-of-symmetry : ∀ x y → x ⊙ y == y ⊙ x
>>>>      proof-of-symmetry = λ x y → definition-of-idenity
>>>> 
>>>> 
>>>>      ========================================================
>>>> 
>>>>      How we  can define a  type "Symmetric Binary Operation"?
>>>>        Having this
>>>>      type we will be able to define ⊙ as
>>>> 
>>>>      _⊙_ : SymmetricBinaryOperation
>>>>      x ⊙ y = A
>>>> 
>>>>      and proof that ⊙ is symmetric will no be required.
>>>> 
>>>> 
>>>>      Best regards,
>>>>      Sergey
>>>>      _______________________________________________
>>>>      Agda mailing list
>>>>      Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>>>      https://lists.chalmers.se/mailman/listinfo/agda
>>>> 
>>>> 
>>>> 
>>>>  --
>>>>  Andreas Abel  <><      Du bist der geliebte Mensch.
>>>> 
>>>>  Department of Computer Science and Engineering
>>>>  Chalmers and Gothenburg University, Sweden
>>>> 
>>>>  andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>>>>  http://www2.tcs.ifi.lmu.de/~abel/
>>>>  _______________________________________________
>>>>  Agda mailing list
>>>>  Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>>>  https://lists.chalmers.se/mailman/listinfo/agda
>>>> 
>>> 
>>> -- 
>>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>> 
>>> Department of Computer Science and Engineering
>>> Chalmers and Gothenburg University, Sweden
>>> 
>>> andreas.abel at gu.se
>>> http://www2.tcs.ifi.lmu.de/~abel/
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda

More information about the Agda mailing list