#丁寧にご説明くださりありがとうございます．
nobsunさんが上に書かれたことは全体としてその通
りだと思います。私もそれらを疑っているのではあり
ません。そういう説明が必要なこと自体を疑問に思っ
ています。
nobsunさんの今回のご説明を参照しながら以下少し
整理してみます。
Queueの代数仕様を書いた人もそれをよく読解した
人も、まさにnobsunさんのご説明のような思考過程
を辿っただろうと思います。逆に、これと同じことを
考えなければ、それを書くことはできないし、それを
よく読解したことにもならないだろうと思います。
しかし、「Queueの仕様でもそれだけの読解努力をし
なければいけない」ということ自体が代数仕様の難点
ではないか、と思うのです。
一般に公理というものは、ある種の自明感があるこ
とが期待されます。そしてその公理系の独立性や完全
性のようなことも見易いことが望ましいと思います。
代数仕様の場合はそれらがいずれも十分でなく、その
ために、いろんなことを考えながら読み書きしなけれ
ばならなくなっているのではないかと思うのです。
たとえば、（まさにお書きになったように）
「frontは最初に登録した要素のこと」／
「backは最初に登録した要素を除いたQueueの
こと」とはじめから書かれていれば、それでほぼ
自明なのですが、いまのQueue代数仕様はそうで
はないので、そこで一つ読解努力や注釈が必要にな
っています。また、「これだけの性質を持っているな
ら．．．キュー(FIFO)として」や「もしこれ以外の
性質で，たとえば，frontとbackの関係がある
とすれば．．．」は完全性に関するご説明ですが、
私もその通りだとー完全だろうと思っていますが、
本当にそうであることをきちんと論証するのは結構
手間がかかるのではないでしょうか（論証に手間が
かかるというのは、すなわち、危ういということに
もなるでしょう）。
いかがでしょうか。
#完全性の問題は難しい問題であるとは思いますが，それは
代数仕様だからというわけではなく，一般的に，自分の欲しい
ものを表現したとき，それが本当に自分の欲しいものを表現し
ているのかという意味と表現の間にある本質的な問題だからです．
ソフトウェアに限らず一般的にいって難問でしょう．
『キューの基本的な考え方は，後ろに1つの要素を追加でき，
（空ではないキューの）先頭から要素を1つとれることにある．』
が示されているとき，Queueの公理で示された性質で十分だと
考えることは実用上合理的だと考えています．
もし，公理から導けないfrontとbackの関係あるいは性質が
クリティカルなのであれば，代数仕様を構成する前の要求に
それが表現されていなければ確認することは不可能ではない
でしょうか．
問題なのは，要求に書かれているにもかかわらず，仕様に
表現されていないことがあることで，それを確認するのが難しい
ことなのですが，これは仕様の書き方に関係なく難しいと思って
います．この意味での危うさのない（あるいは少い）手法という
ものがあるかどうかは知りませんし，私自身は思いついてはいません．
なにかよいアイデアはありますでしょうか．
代数仕様が関数プログラミングと相性がよいのは（具体的な仕様が
自分の欲しいあるものがもつべき性質を表現していると思えるなら）
実装がその性質を満しているかどうかは形式的に確認できることです．
haskell-ja > Archives > 2012/11/09