総称ラムダとかを参考にすると、次のようになる。ただし、これは厳密結合の推論で、型制約が出てこない。残念ながら、これでは実用にならないが、キレイにまとまる感じはある。S, Tなどは型項（または型表現）、f, gなどはコマンド項、M, Nなどは式（formula…

ベックの法則の定式化がけっこう分かってきた。これはさすがに書いておかないとな。忘れるからな。基本的に（メンタルに）想定しているのは多元環Rと加群Mなんだが、モノイドとモノイド作用なら何でも同じこと。ここでは、モノイド構造さえ考えないでマグマ…

http://www.cs.cornell.edu/~kozen/papers/papers_collapsed.htm ここからいろいろな論文が取れる。set expressionはtype expressionで、set constraintsはtype constraintsだから、そのまま型推論に使える。しかし、termset代数が、エルブラン方式理論であ…