型のある数式
$ \sum_{k=1}^n f(k)\sum_{k=1}^n f(k)をどのように型付ければよいのか
まずは素朴に3変数関数Sumとして
Sum(k=1,n,f(k))と考える
引数
k=1
kの初期値設定
n
nという整数
f(k)
kを含みうる関数
そもそも数式にセマンティクスがいるのか？
表示するだけなら数式に計算させる必要は一切ない
コンピュータ上で数式の組版をする（すなわち適当な数式マークアップ言語で記述する）とき、せめてもう少しヒントぐらい出ても良いのではないかと常々思う
関数$ f(v)は自然数を引数に取るが、$ vは自然数とは明らかに定義しなかったので、おかしい
が、どうすれば良いバランスになるのかわからない
各々人で書き方の流儀は全然異なるので普遍的なものは作れなさそう
ユーザー及びドキュメントの粒度でいちいち制約を書く必要がありそう
そのコストと釣り合うメリットがあるかはわからない
補完が効けば結構良いか？
数学上のプリミティヴな操作に対応した制限文法
定義する
証明する
補題/定理/etcを利用する
数学言語学，数学言語処理（mathmetical linguistics, mathmetical language process） 長編論文に登場する数式に一個一個頑張って意味を与えてコーパスを作ろうとする試みについて