Gabriel Gonzalez 氏の Equational Reasoning を読んだメモ - relations -> transitive
自分も「プログラマのための等式推論」的な記事書いてみたいとか思っていて、手頃な記事を氏が最近書かれていたのを思い出し、注意深く読むことにした。素人がちょっと分かったつもりになると人に教えたがるアレな病気を発症してるのです。 Haskell for all: Equational reasoning 手で式を置き換えることによって Haskell のコードは解釈できる 等式から等式へ置き換えて式を解釈することを等式推論 (equational reasoning) という Haskell では左辺と右辺は相互に置換可能 x = 5 という宣言をしたとする。このときプログラム中に x を見つけたら機械的に 5 に置き換えてよい (substitution) 。同様に 5 を見つけたら x に置き換えてよい Haskell ではこのような置き換えを行ってもプログラムのふるまいは変わらない (参照
sbv
sbv: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Express properties about Haskell programs and automatically prove them using SMT (Satisfiability Modulo Theories) solvers. [Skip to Readme] DataData.SBVData.SBV.CharData.SBV.ControlData.SBV.DynamicData.SBV.EitherData.SBV.FloatData.SBV.InternalsData.SBV.ListData.SBV.MaybeData.SBV.RationalData.SBV.RegExpData.SBV.SetData.
定理証明系 Haskell
この記事は Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 二十日目の記事であり、更にTCUGの新刊「Coqによる定理証明」の販促記事でもある。 型システム再考 Haskell は静的型付き言語だ。それだけでなく、強力な型推論や表現力の高い型システムを備えている。 型とは何だろうか。 こうした質問に対してよくある答えは、「値の種類を区別するためのタグ」になるだろうか。Int型は整数だし、Bool型は真偽値で、[Int]型は整数値リストを表す型だ。なるほど、値の種類を区別するものに見える。 しかし、この答えは間違ってはいないが、もっと相応しい云い方が出来るだろう。それは、「型は不変条件である」というものだ1。この言明は別に私固有の見方というわけではなく、ある程度の型レベルプログラミングをやった事のある人
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
