LTSA - Labelled Transition System AnalyserLTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA suppor…

Soundness In mathematical logic, a logical system has the soundness property if and only if its inference rules prove only formulas that are valid with respect to its semantics. In most cases, this comes down to its rules having the proper…

In computer programming, an algebraic data type (sometimes also called a variant type[1]) is a datatype each of whose values is data from other datatypes wrapped in one of the constructors of the datatype. Any wrapped datum is an argument …

A data type (or datatype) in programming languages is a set of values and the operations on those values.

Wikipedia によると、 形式仕様記述とはソフトウェアやハードウェアの実装を開発する際に使用される数学的記述。 数学的に書くと何がいいのか？

1.1 Models of computation Some mathematical functions are computable and some are not: There are problems for which no computer program can provide a solution even assuming that the amount of time and space available to carry out the compu…

モジュールもじゅーる 【モジュール】 moduleハードウェアやソフトウェアを構成する個々の部品のこと。ハードウェアのモジュールの場合、基板1枚1枚などそれ単体が高い機能を持った、入れ替え可能な部品を指す。ソフトウェアのモジュールの場合、プログラム…

定理1.4.6 は論理式の形だけを見れば論理値を考えなくても適用できるようになっている。この節では、意味を考えなくても、決められた式の変形だけで正しい命題を作成できるような規則を与える。記号列の集合を形式的な規則で定義したものを形式的体系（formal…

上記の条件を満たす「Γ|=φ」の形の「行」を証明（Proof）と呼ぶ。とくに、一番最後に書いてある式が証明された式である。 条件：どの「行」もそれがすぐに正しいことがわかるか、それ以前に現れる「行」をいくつか見ればすぐに正しいことがわかる。さらに注…

恒真命題 （Tautology） 論理式φがφに現れる命題変数の任意の解釈で真になるとき“|= φ”と書き，φを恒真命題と呼ぶ． 意味論的帰結（） 論理的推論は「→」に着目すると見やすくなるので，次のような定義をする．論理式Γ，φに大使，「Γ→φ」が恒真命題のとき「Γ…

フルスタックフレームワークとはUIやDB、セキュリティなどの基本的な問題領域にAll in oneな環境を提供するもの各コンポーネント毎のフレームワークではそれらを組み合わせて動作させることに一定以上の複雑さが有り、特別なノウハウが必要となる。フルスタ…

フレームワークとは 【framework】 - 意味/解説/説明/定義 ： IT用語辞典 http://e-words.jp/w/E38395E383ACE383BCE383A0E383AFE383BCE382AF.html ソフトウェアの世界では、アプリケーションソフトを開発する際に頻繁に必要とされる汎用的な機能をまとめて提…

モジュール (Module)とは、工学などにおける設計上の概念で、システムを構成する要素となるもの。いくつかの部品的機能を集め、まとまりのある機能を持った部品のこと。モジュールに従っているものをモジュラー (modular)という。入出力を絞り込み、標準化す…

トランザクションとは 【transaction】 - 意味/解説/説明/定義 ： IT用語辞典 http://e-words.jp/w/E38388E383A9E383B3E382B6E382AFE382B7E383A7E383B3.html トランザクションとは、関連する複数の処理を一つの処理単位としてまとめたもの。金融機関のコンピ…

http://www.atmarkit.co.jp/news/analysis/200707/17/trans.html : トランザクションメモリはマルチコアの救世主となるのか？ − ＠IT これに対して、1993年にMaurice Herlihy氏とJ.Eliot B. Moss氏が提案したコンセプトがトランザクションメモリ（Transactio…

「Why "Concurrency" matters?」と題して、ソフトウェアにおける並行性・並行概念（以下、並行性）の大切さについて考えてみたい。まず、なぜ並行性が重要かを、ずばり一言で述べる。それは『「並行性」はシステムの複雑性を「簡素化」することができ、すな…

Function call と Message Passing は異なるプロセス間通信概念・手法だと思えてきた。 OOP では、Function Call を用いる。CCSやCSPや、その実装であるPromela などでは、Message Passing を用いているとか？さらに言うと、Message Passing の方が、仕様記…

充足関係を、構造と閉論理式の集合との関係について拡張できる。T が 言語 L の閉論理式の集合で、M が L-構造のとき、M |= T とは、T に属する任意の閉論理式 p に対し、M |= p となることである。このとき、M を T のモデルと呼ぶ。また、閉論理式の集合を…

言語 L の任意の閉じた論理式の集合を「理論」と呼ぶ。

記号列の集合を形式的な規則で定義したものを形式的体系（formal system）と呼び、記号列がその集合に属することをこの形式的な規則に沿って、示したものをその体系における証明と呼ぶ。

ついでに、何かを書き込もうとしたのであった。 以上

Haskell Haxml の使い方は以下の論文に詳しく書いてある（っぽい）。Haxml のサンプルコードがあんまりないみたいなので参考になる。ただバージョンが少しずれてるので注意。http://www.cs.york.ac.uk/fp/HaXml/この論文ってICFP99で発表されてるんですかね…

Haskell Haxml モジュールを用いたサンプルコードを書いてみた。下のXML文書中のタグの中身をプリントする。・Haskell コード import System.IO import System.Environment import Text.XML.HaXml import Text.XML.HaXml.Pretty (content) main :: IO () mai…

Haskell で XML ファイルを入出力する作業が必要になった。というわけで、Haskell の XML Parser を調べ見ると、HXT (Haskell Tool Box) というのが標準的だそうな。というわけで、早速 Windows XP上にインストールしてみる。のだが、なかなかうまくいかない…

Haskell のお勉強をした。Agda の経験があるから、すんなりと理解できた（ように思う）。実際ゴリゴリ書こうとすると、いろいろとボロが出るんだろうが。ギターを習うときに、最初にFを鳴らす練習をすればいいといっていた人がいた。F で挫折する人が多いか…

勉強するときや読書するときなど、本に線を引いたり、本に書き込む人っていますよね。僕はあれってどうかなと思います。というのも、本は何回も読むものだと思うのですが、前に引いた線のせいで本が読みにくくなります。特にカラフルになってたりすると、次…

これまではライブドアでブログかいてたんですけど、今回ははてなダイアリーで書くことにしました。その決め手は、使い心地です。 はてダは直接編集できていい感じだね。