>>895
一般的に双対を扱うためにGrothendieckがとったアプローチは理論内部での定理でなく、
理論を抽象化するメタ定理の証明に使用する圏と射を導入したんだよね。
それによって公理系の性質に関するメタな証明をEGAやSGAで実行したのは有名だよね。
これは、無限２分木がかならず無限の道をもつという弱ケーニヒの補題を公理に加えた体系WKL_0となり
Lisp/Schemeでは欠けている言語的特長を付加することを意味する。
例えるならフェルマーの定理の証明でワイルズがやったようなS式版のコホモロジーと指標の対応をつけてやることに相当する。
それが上で言ったメタ定理に使用する圏と射を一段下のレベルで実行することで、
Grothendieck流ならもう一段抽象レベルでプログラム出来なければいけないことになる。

それと別に線型空間の双対空間やアーベル群の双対などのポントリャーギン双対との類似物はもっと単純で、
それらの双対性用のライブラリーを作成する単純作業で、それをS式で考えるなら、マクロ生成マクロを用意するのが一つの手段。
グレブナー基底を取り替えるような感じだね。
証明するなら枠外にはみ出すけど結果を使うだけなら、それらはLisp/Schemeを言語的にはなんら拡張するような話ではない。