はてなグループの終了日を2020年1月31日(金)に決定しました - はてなの告知
はてなグループの終了日を2020年1月31日(金)に決定しました 以下のエントリの通り、今年末を目処にはてなグループを終了予定である旨をお知らせしておりました。 2019年末を目処に、はてなグループの提供を終了する予定です - はてなグループ日記 このたび、正式に終了日を決定いたしましたので、以下の通りご確認ください。 終了日: 2020年1月31日(金) エクスポート希望申請期限:2020年1月31日(金) 終了日以降は、はてなグループの閲覧および投稿は行えません。日記のエクスポートが必要な方は以下の記事にしたがって手続きをしてください。 はてなグループに投稿された日記データのエクスポートについて - はてなグループ日記 ご利用のみなさまにはご迷惑をおかけいたしますが、どうぞよろしくお願いいたします。 2020-06-25 追記 はてなグループ日記のエクスポートデータは2020年2月28
Agda2におけるPropとSet0の違い
Üe🦀 @ranha @ikegami__ 多分私のは、組込みの力で「便利になった」ようなequalityが欲しいなーっていう言い換えで2例作っただけな気がします。ただSet0とPropの違いは知りたいです！ 2010-03-28 07:14:19 Ikegami Daisuke @ikegami__ あ、Set0 と Prop の違いはわたしが答えられます : Martin-Loef の型理論では Set0, Set1, Set2, ... : "Proposition as a set" : という概念から、命題は Set0 の型を持つのですが、Set0 と書くと(つづく) 2010-03-28 07:16:25 Ikegami Daisuke @ikegami__ 命題は Set0 の型を持つのですが、Set0 の使い道は命題だけとは限らないので、命題の型は Prop と、別名をつ
Sequent Calculus in Haskell
A Theorem Prover for Intuitionistic Propositional Logic One of the standard textbooks for ML, the "other" functional programming language, is Paulson's ML for the Working Programmer. Some years back, this is the book that I first learnt functional programming from. The book culminates in a theorem prover for classical first order logic, which is the kind of task that functional programming languag
書評（数理論理学）
一般解説書など 結城浩：数学ガール／ゲーデルの不完全性定理, ソフトバンククリエイティブ (2009) (はてなダイアリーの記事に加筆修正して転載) 本書は、数学の定理の解説としてはきわめてまっとうな、ゲーデルの不完全性定理の解説本である。普通なら、まっとうであることは評価の最低基準であって、それだけで高評価になるものではない。しかし、不完全性定理に限ってはそうはいえない。ちまたにあふれる不完全性定理に関わる言説にはまっとうでないものがあまりにも多い。そのため、不完全性定理の解説本はまっとうであるだけで高い評価を得てしまう。 まっとうであるために第一に必要なことは、内容に初歩的な間違いがないことである。当たり前のことだが、その当たり前が実現できていない不完全性定理本は多い。肝心の「不完全」の定義を間違えているものすら珍しくない。その点、本書は正しく記述しているのみならず、ちまたによくある濫
C++で論理型言語コンパイラを書いてみる
C++ で、論理型言語(GHC)コンパイラを書く 論理型言語コンパイラを作る理由 基本ポリシー: いろいろ諦める GHC の基本 実装関連 C++ を使う理由 論理変数を実装する ゴールのコンパイル ゴールキューと疑似マルチタスク 疑似マルチタスクから本当のマルチタスクへ 最適化 ガベージコレクション Boehm GC を C++ で使うための調査 ガベージコレクションの実装 JavaScript で GHC [JavaScript] 8-queen [JavaScript] Canvas を使った描画 [JavaScript] 組み込み述語の書き方 (メモ) KLIC との比較 GraphViz と GHC オブジェクト構造の可視化(案) GraphViz によるグラフィカルデバッグ GHC プログラミング 入出力と順序制御 竹内関数と遅延評価 [JavaScript] wait/1 と
d.y.d. 文字コード＆ベイズ推定
12:21 06/05/28 うたひめ 先日の記事に書いたように KOKIA にハマりまして、 とりあえず片っ端から聴いてみることにしました。まずは 1st アルバムの 『songbird』 から … …４曲目の "白い雪" ヤバい。超ヤバい。なんだこれ。ツボすぎる。 ベスト盤を聴いたとき感じた揺らぎなく落ち着いた歌唱力的な曲を期待して聴きはじめたら、 予想外の声質の歌が飛び込んできてびっくりしました。もちろん抜群に巧いのに かわりはないんですが、ずっと儚げな、ガラス細工みたいなイメージの、ああ、その、 つまり白い雪みたいな雰囲気の綺麗な声で。その声と奇跡的にマッチしたメロディ。 すごいなあ。９曲目の "ありがとう…" もベスト盤でのリテイクと比べて同じ印象で、 Amazonのreview で TenderBerry さんという方が近いことを書いておられました。 しかし書いてて自分の語彙の
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
セキュアコーディング(法政大学 理工学部 応用情報工学科 2年次後期 (2010年度))
数理科学的バグ撲滅方法論のすすめ---目次 | 日経 xTECH（クロステック）