いま私が作ってる定理証明支援系はちょうどS式のよさを引き出してると思う。手動(いつか自動に…)でS式を書き換えていって真に置き換えることを目指すやつなんだけど、S式のプログラムによる扱いやすさと人から見たときの分かりやすさが両立してて素晴らしい。特に目で見て人が木と理解できる構文なので書き換えたい式の位置を指定するのが簡単なのです。
いま私が作ってる定理証明支援系はちょうどS式のよさを引き出してると思う。手動(いつか自動に…)でS式を書き換えていって真に置き換えることを目指すやつなんだけど、S式のプログラムによる扱いやすさと人から見たときの分かりやすさが両立してて素晴らしい。特に目で見て人が木と理解できる構文なので書き換えたい式の位置を指定するのが簡単なのです。
senooken JP Social is a social network, courtesy of senooken. It runs on GNU social, version 2.0.2-beta0, available under the GNU Affero General Public License.
All senooken JP Social content and data are available under the Creative Commons Attribution 3.0 license.