2014-06-04から1日間の記事一覧

2つの自然数列を結合したものの要素数が夫々の自然数列の要素数の和に等しいことの証明

Coq

Inductive nat_list : Set := NNil : nat_list NCons : nat -> nat_list -> nat_list. Fixpoint nlength (ls : nat_list) : nat := match ls with NNil => O NCons _ ls' => S (nlength ls') end.Fixpoint napp (ls1 ls2 : nat_list) : nat_list := match ls…

次世代電子契約及び分散型応用ソフトウェア基盤#01

2009年1月、Satoshi NakamotoがBitcoinのブロック鎖（blockchain）を最初に作動させたとき、同時に彼は当時未だ試されたことのなかった急進的な概念を2つ導入していた。1つは「Bitcoin」、即ち、固有の価値や中央発行者のような裏付けを持たずして価値を維持…