Re: Concatenation of finite sequences

Dear Andrzej,

I am in favour of ^' becasue

   - it was introduced first (by me in a work with Y. Nakamura ;-),
   - is defined through -cut which is independently useful.

I remember your surprise when we learned about this almost a repetition in
1996.

Cheers, PR


2011/1/11 <[email protected]>

> Quite often we need to concatenate finite sequences f and g under the
> assumption that the last element of f equals the first element of g and we
> do not want it to be repeated. Let f = (x_1, .. x_m), g = (x_m,..., x_n)
> then the result should be
>      (x_1, ..., x_n)
>
> In MML two such functors had been introduced:
>
>  let p,q be FinSequence;
>  func p$^q -> FinSequence means
> :: REWRITE1:def 1
>  it = p^q if p = {} or q = {} otherwise
>  ex i being Element of NAT, r being FinSequence st len p = i+1 & r = p|Seg
> i &
>  it = r^q;
>
> and
>
>  let p, q be FinSequence;
>  func p ^' q -> FinSequence equals
> :: GRAPH_2:def 2
>  p^(2, len q)-cut q;
>
> If we neglect the problem of empty sequence (the operation is meaningless
> in such a case anyway) the big difference is that in p $^ q the last element
> of the first sequence is removed and in p ^' q the first element of the
> second one is removed.
> In the interesting case (when they coincide) the result is the same. So, to
> keep the integrity of MML we should remove one of the definitions. The
> problem is which one?
>
> What do you think?
>
> Regards,
> Andrzej
>
>


-- 
Piotr Rudnicki
http://www.cs.ualberta.ca/~piotr <http://www.cs.ualberta.ca/%7Epiotr>