Maude-help mailing list

[Francisco Duran <duran AT lcc.uma.es>]

> Here's what I would like to write:
>
>     sort BalancedListPair{X,Y} .
>     subsort BalancedListPair{X,Y} < (List{X},List{Y}) .
>
>     cmb (LX,LY) : BalancedListPair{X,Y} if size(LX) = size(LY) .
>
>     op _zip_ : BalancedListPair{X,Y} -> List{(X,Y)} .
>
> In other words, I want product types and tupling such that any n-ary
> operator is equivalent to a unary operator on n-tuples.

Hi Matthias,

Maude doesn't support such facilities, and actually we haven't consider 
so far including them.

This code mixes two things, you have changed both the notation for 
naming sorts and the tuple constructors.

Changing the way of naming sorts is tricky. Currently we can have either 
simple (single-identifier) or parameterized sorts (sorts of the form 
s{V1, ..., Vn} with V1...Vn views). Therefore, you must write

    sort BalancedListPair{X, Y} .
    subsort BalancedListPair{X, Y} < Tuple{List{X}, List{Y}} .

    op zip : BalancedListPair{X, Y} -> List{Tuple{X, Y}} .

The notation for operators is very flexible however. In fact, the 
notation for 2-tuples is (_,_), thus being possible to write

    cmb (LX, LY) : BalancedListPair{X, Y} if size(LX) = size(LY) .

I nevertheless prefer your first option, and I don't understand why you 
discarded it. In general, for dealing with exceptional situations like 
the one you wish to consider, you have two options, namely reducing the 
arity (the one you like) or extending the coarity of your operators.

By declaring your _zip_ operator like

    op _zip_ : List{X} List{Y} -> [List{Tuple{X, Y}}] .

you are saying that you may have "valid" lists that may lead to error 
terms in the kind [List{Tuple{X, Y}}]. You are also restricting the 
applicability of your operator, either by saying

     eq LX zip LY = LX zipHelper LY if size(LX) = size(LY) .

as you did, or just by defining _zip_ as

    eq (EX LX) zip (EY LY) = (EX, EY) (LX zip LY) .
    eq nil zip nil = nil .

Notice that in both cases, you get a similar result for exceptional cases:

Maude> (red in BLP1{Nat, Nat} : zip((1 3 5, 2 4 6 8)) .)
result `[List`{Tuple`{Nat`,Nat`}`}`] :
  [1,2][3,4][5,6]zip((nil,8))

Maude> (red in BLP2{Nat, Nat} : (1 3 5) zip (2 4 6 8) .)
result `[List`{Tuple`{Nat`,Nat`}`}`] :
  (1,2)(3,4)(5,6)(nil zip 8)

that is, zipping list of different lengths results in error terms. I put 
the whole specs below so yuo can play with them.

Best regards,

Paco Durán

---------------------------------o-------------------------------------

(view Tuple{X :: TRIV, Y :: TRIV} from TRIV to TUPLE[2]{X, Y} is
  sort Elt to Tuple{X, Y} .
 endv)

(view List{X :: TRIV} from TRIV to LIST{X} is
  sort Elt to List{X} .
 endv)

(fmod BLP1{X :: TRIV, Y :: TRIV} is
    pr TUPLE[2]{List{X}, List{Y}} .
    pr LIST{Tuple{X, Y}} * (op `(_`,_`) to `[_`,_`]) .

    sort BalancedListPair{X, Y} .
    subsort BalancedListPair{X, Y} < Tuple{List{X}, List{Y}} .

    var LX : List{X} .
    var LY : List{Y} .
    var EX : X$Elt .
    var EY : Y$Elt .

    cmb (LX, LY) : BalancedListPair{X, Y} if size(LX) = size(LY) .

    op zip : BalancedListPair{X, Y} -> List{Tuple{X, Y}} .

    eq zip((EX LX, EY LY)) = [EX, EY] zip((LX, LY)) .
    eq zip((nil, nil)) = nil .
 endfm)

(red in BLP1{Nat, Nat} : zip((1 3 5, 2 4 6)) .)

(red in BLP1{Nat, Nat} : zip((1 3 5, 2 4 6 8)) .)

(fmod BLP2{X :: TRIV, Y :: TRIV} is
    pr LIST{Tuple{X, Y}} .
    pr LIST{X} .
    pr LIST{Y} .

    var LX : List{X} .
    var LY : List{Y} .
    var EX : X$Elt .
    var EY : Y$Elt .

    op _zip_ : List{X} List{Y} -> [List{Tuple{X, Y}}] .

    eq (EX LX) zip (EY LY) = (EX, EY) (LX zip LY) .
    eq nil zip nil = nil .
 endfm)

(red in BLP2{Nat, Nat} : (1 3 5) zip (2 4 6) .)

(red in BLP2{Nat, Nat} : (1 3 5) zip (2 4 6 8) .)