• ε: seq T

  • _ \vartriangleright _ : seq T ×T → seq T

  • _ \vartriangleleft _ : T ×seq T → seq T

  • _ ·_ : seq T ×seq T → seq T

  • 〈 _ 〉 : T → seq T

  • 〈 _,…,_ 〉 : Tn → seq T

   - preferably one-to-one
  • Gseq T = {ε, \vartriangleright }, GUseq T = {ε, ε\vartriangleright a, ε\vartriangleright b, …, ε\vartriangleright a \vartriangleright b, …}

  • G′seq T = {ε, \vartriangleleft }, GU′seq T = {ε, a \vartriangleleft ε, b \vartriangleleft ε, …, b \vartriangleleft a \vartriangleleft ε, …}

  • G"seq T = {ε, ·, 〈 _ 〉 }, GU"seq T = {ε, 〈 a 〉 , 〈 b 〉 , ,…, ε·ε, …, ε·〈 a 〉 , …}

  
  • G"′seq T = {ε, 〈 _ 〉 , 〈 _ , _ 〉 , …}, GU"′seq T = {ε, 〈 a 〉 , 〈 b 〉 , ,…, 〈 a,a 〉 , …}


slide: The ADT Seq