search

kmyk-jikka / Jikka

an automated solver for problems of competitive programming
https://kmyk-jikka.github.io/Jikka/playground
Apache License 2.0
151 stars 12 forks source link

TODO: 型について #2

Closed kmyk closed 3 years ago

kmyk commented 5 years ago

構文解析はだいたいできたので、型が付いていない λ 項が入力されていると見ることができる。したいのは式木を組み換えての最適化処理。なのでとりあえずいい感じに型再構築が必要。

kmyk commented 5 years ago

型再構築の意味でもその後の利用の意味でも、依存型っぽくやるよりも篩型っぽくやる方がよいらしい。 z3 などの SMT solver でえいってするとかなんとか。その後の最適化部分はたぶん手動での探索になりそう？ https://7colou.red/blog/2018/07-07-difference/index.html

kmyk commented 5 years ago

細かい制約の表現や最適化をしようと思うと refinement types 相当の処理は避けられなさそう。単に静的解析というより自動定理証明よりの大域的な最適化をやろうとしてるのだから、どうやっても型はついてまわるはず。自然に篩型に近付くはずなのでひとまずまだ ad-hoc に進めて、適当なタイミングでリファクタリングという形で篩型を実装する感じでやりたい。 = とかをいい感じに多相にしたい問題については、Haskell にならって type class をすることになりそう。列多相 row polymorphism も教えてもらったが、今回はこれは違う気がする。

kmyk commented 5 years ago

以下の論文を読んで Liquid Types を実装するのが次の課題です

Rondon, Patrick M., Ming Kawaguci, and Ranjit Jhala. "Liquid types." ACM SIGPLAN Notices. Vol. 43. No. 6. ACM, 2008.

kmyk commented 5 years ago

まずは最適化部分抜きのもっと小さな処理系を書いて練習します https://github.com/kmyk/liquid-types-example