4日前15 min
代数的データ型
代数的データ型 (algebraic data type、ADT) は、既にある型を「かつ」(直積) と「or」(直和) で組み合わせて作る型。 新しい型を作る方法は、突き詰めると2つしかない。 直積 (product): A の値 かつ …
最新の記事
78 件中 1–10 件
型付きラムダ計算
単純型付きラムダ計算 (simply typed lambda calculus) は、関数の定義と適用だけからなる最小のプログラミング言語 (ラムダ計算) に型を付けたもの。 型が付いた項は「関数でないものを呼ぶ」「Boolに数を渡す」と…
モデル検査
モデル検査 (model checking) は、初期状態と遷移規則から到達可能な状態をすべて列挙し、仕様に反する状態がないかを自動で確かめる手法。 入力は次の2つ。 モデル: システムを有限の状態遷移系として書いたもの 仕様: 「2つのp…
Jujutsu
Jujutsu (jj) はバージョン管理システムで、Git repositoryをそのまま扱える。 Gitとの一番の違いは、commitを後から直す前提で設計されていること。 Git: 一度commitしたら直さない前提。直すには com…
全身麻酔と臨死体験から考える意識
全身麻酔は、脳が正常に動いているのに意識だけが消える。 臨死体験 (near-death experience; NDE) は、脳がほとんど動き得ない状況で意識が生じたと報告される。 正反対の現象だが、どちらも脳の発火と意識の対応が素直でな…
意識は本当に脳が作っているのか
「意識は脳の電気信号が作っている」はほとんど常識の扱いを受けているが、この常識はかなり薄い根拠に乗っている。 意識と自由意志について、私が引っかかっている点を並べてみる。 脳の発火と意識体験の対応は、麻酔・脳損傷・脳刺激といった介入でも再現…
ブラック・ショールズ方程式
確率微分方程式 とある金融商品を特定の時点で購入する権利を ヨーロピアン・コール・オプション (European call option) という。 ヨーロピアン・コール・オプションは、とある金融商品を特定の時点で (ヨーロピアン) 購入す…
量子計算
量子ビット を観測すると、確率 ||^2, ||^2 で状態 0, 1 が得られる。 0 = 1 0 + 0 1 を観測すると、確率 |1|^2 で 0 が得られる。 つまり、確実に 0 が得られる。 1 = 0 0 + 1 1 を観測する…
秘匿計算
モジュラ逆数 (modular multiplicative inverse) とは、互いに素な整数 a, m に対して を満たす整数 x のことである。 中国剰余定理 (Chinese Remainder Theorem, CRT) とは…
情報理論
(自己) 情報量 (entropy) とは、情報理論の概念で情報の「稀少さ」を表す指標である。 情報が稀少であるほど、情報量は大きくなる。 ある事象 E が起こる確率を p(E) とすると、その情報量 i(E) は次のように定義される。 前…