Peirce's Law Equivalent to Law of Excluded Middle - ProofWiki
Theorem Peirce's Law: $\left({p \implies q}\right) \implies p \vdash p$ is logically equivalent to the Law of Excluded Middle: $\vdash p \lor \neg p$ That is, Peirce's Law holds if and only if the Law of Excluded Middle holds. Law of Excluded Middle implies Peirce's Law Let the truth of the Law of Excluded Middle be assumed. Then: $\left({p \lor \neg p}\right) \vdash \left({\left({p \implies q}\ri
zsh の zmv を使って簡単に複数ファイルを一括リネームする - mollifier delta blog
連番のファイルがずらーっとあったとき、複数のファイル名を一気にスマートに変えたいことがある。一個ずつちまちまリネームなんてやってられない。そんなときは zsh の zmv を使うと便利なので紹介する。 zmv で何ができるか 例えばこんな感じで 1.txt から 6.txt までファイルがあったとする。 % ls 1.txt 3.txt 5.txt 2.txt 4.txt 6.txtでも、ファイル名短すぎてわかりにくいなー、file-1.txt みたいに頭に file ってつけたいなー、って思ったとしよう。 そんなときのために zsh には zmv ってコマンドがあって、この手の一括リネームがスマートにできる。お手軽な使い方はこんな感じ。 あらかじめ ~/.zshrc にこう書いておいてから、 autoload -Uz zmv alias zmv='noglob zmv -W' 一回のコマ
X86アセンブラ/x86アーキテクチャ - Wikibooks
x86アーキテクチャは、インテルが開発したマイクロプロセッサのアーキテクチャです。1978年に最初のx86プロセッサであるIntel 8086が登場して以来、x86アーキテクチャはPCおよび互換機市場で非常に広く普及しています。 このアーキテクチャは、以下のような特徴を持っています。 命令セット x86アーキテクチャは複数の命令セットを組み合わせています。初期のバージョンから現在のx86-64まで、多くの命令が追加され、命令セットが拡張されてきました。 互換性 x86プロセッサは、過去のアーキテクチャとの互換性を保持しています。これは、古いソフトウェアやシステムが新しいx86プロセッサで動作することを可能にしています。 アドレッシングモード x86アーキテクチャは複数のアドレッシングモードを持ち、メモリアクセスやデータ処理の柔軟性を提供しています。 セグメンテーション x86ではセグメンテ
Haskell/カリー=ハワード同型 - Wikibooks
カリー=ハワード同型(Curry-Howard isomorphism)は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。 導入[編集] これよりカリー=ハワード同型は単に C-H と表記する。C-H が示しているのは、定理の本質を反映するような型を構築し、それからその型を持つ値を見つけさえすれば、どんな数学的定理をも証明することができる、ということだ。これは最初は極めて不思議に思える。型と定理にどんな関係があるというのだろうか？しかしながら、以下に述べるように、このふたつは非常に近しい関係にあるのである。はじめる前に簡単に注意しておくが、導入の章では error や undefinedのような 表示的意味論 が ⊥ である式の存在は無視する。これらはとても重要な役割を果たすのだが、これらについては後ほど別に考えることにする。また、unsafeCo
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Technical Note TN2123: CrashReporter
https://www.haskell.org/wikiupload/1/14/TMR-Issue6.pdf
