述語論理で、ドモルガンに相当すんのが以下の4つ ¬(∃x,P x) -> ∀x,¬ P x ∀x,¬ P x -> ¬(∃x,P x) ∃x, ¬ P x -> ¬(∀x,P x) ¬(∀x,P x) -> ∃x, ¬ P x 例によって最後のやつが排中律or二重否定則とかないと証明出来ないらしい。 Require Import Coq.Logic.Classic…

命題論理ドモルガン4兄弟 ¬(A ∨ B) → ¬A ∧ ¬B. ¬A ∧ ¬B → ¬(A ∨ B). ¬A ∨ ¬B → ¬(A ∧ B). ¬(A ∧ B) → ¬A ∨ ¬B.のうち、直観主義論理の範囲で証明出来ないらしい ¬(A ∧ B) → ¬A ∨ ¬B.の証明。 排中律を前提とする。排中律を使って、A∨¬AとB∨¬Bをコンテキスト…

一年前のものを見直すとひどいな。InductiveとDefinitonの区別が明らかについてないのとか。というか、なんで今区別つくようになってんだ。自分。

夏休みに「software foundation」を読み返している。もう読み始めて何年たってるのか。前読んでた時から半年とか空くと全部忘れてるのでまた読み直しが発生して、とかの悪循環。どんどん後退している。年も食ってるし。以前の自分の解答で諦めてたらしい(諦…

jsの比較的新しい機能のPromiseとasync/awaitを使って非同期関数を同期関数っぽくみせかけることが出来る。たとえば、jquery uiのconfirmダイアログをwindow標準のconfirmと似たような使い勝手にすることも一応可能。 function myconfirm_promise() { var pr…

スマリヤンの数理論理学の本を斜め読みしてて、コンパクト定理のとこでわけが分からなくなって放置してたんだけど、最近読み直して、なんとなくその時なぜ分からないと思ったのかが分かったような気がする。本の構成上、その直前まで木について説明が続いて…

麻薬使用者を憐んであげますというエントリ http://fujipon.hatenablog.com/entry/2016/10/27/011319ブックマーク http://b.hatena.ne.jp/entry/fujipon.hatenablog.com/entry/2016/10/27/011319大麻取締法の時効は七年だそうで、もう時効だから書きますが、…

仕事がつまらんので逃避中。https://www.cis.upenn.edu/~bcpierce/sf/current/ 読み始めて三年の月日が経とうというのに、まだ半分もいかない。 ちょっと読んでは分からんので中断し、忘れているので最初からやりなおしとかやってりゃ進まないのは当たり前。…

この一週間くらい手を動かしてた、Software Foundationsの「サブシーケンスという関係は推移的である。」ということの証明が出来た!めっさうれしい。 Inductive subseq : list nat -> list nat -> Prop := | subseq_nil : subseq [] [] | subseq_e : forall …

死ぬほど面倒くさい。 検証環境で中間証明書から発行されたオレオレサーバ証明書を作ろうとして嵌る。テキトーにコマンドでオレオレ証明書発行して、nodejsのexpressサーバに中間証明書を設定すると、 chromeブラウザからの検証でエラーになって、強制的にペ…

clojureScriptを触るついでに。 clojureScriptはまださわれていない。会社のproxy環境下でいろいろ動かなかった。 Light Tableでpluginの一覧が取れない。proxyパスワード存在下ではそもそもまだ動かないみたいだ。 leiningenはproxyパスワードに:が入ってた…

scalaコマンドによるreplとscalacコマンドでコンパイル出来るコードに違いがある？Noneとかnil周りを自前で定義するような基本的なコードは、あまりreplで動かない？Scala関数型デザインの本はあまりscalaコマンドぽちぽち叩く人向けではないのかもしれん。r…

Scala関数型デザイン&プログラミング―Scalazコントリビューターによる関数型徹底ガイド作者: Paul Chiusano,Rúnar Bjarnason,株式会社クイープ出版社/メーカー: インプレス発売日: 2015/04/30メディア: Kindle版この商品を含むブログ (3件) を見るこの本が基…

どっかに 引数を一個だけ渡すメソッド呼出しでは、引数を囲む括弧を丸括弧から中括弧に変えてもよいことになっている。とか書いてあった。つまり、 println("hello world") は、 println ｛ "hello world" ｝ と書いてもよい。と。 引数が関数リテラル一個で…

本家 http://docs.scala-lang.org/少しは日本語もあるみたい。Sbtビルドシステム http://www.scala-sbt.org/0.13/docs/play2 https://www.playframework.com/documentation/2.4.x/Homegoほど日本語で読めるのドキュメントがまとまってない感じ。 チュートリ…

scalaは関数がfirst classオブジェクトなので関数を引数に渡したり出来る。今まで触ってきた言語(coq除く)は型なしの言語ばかりだったので、戸惑うこと多し。 def test(f:(Int => Int) { f(100) } test(x=>x+100) // Int = 200 test{x=>x+200} // Int 300 //…

仕事でplay2を触るらしい。多分scalaではないと思うが。いい機会だからscalaも触ってみようかと。とりあえず、class と object var と valを 覚えた。classとobjectの関係は、jsのobjectとプロトタイプみたいなもんらしい。 jsのプロトタイプって自分から使…

先日のやつより、以下の量化子に対するタブロー規則が得られる。 からが得られる。aは任意のパラメータでよい からTφ(a)が得られる。aはまだ使われてないパラメータでなければならない。 F∀xφ(x)からTφ(a)が得られる。aはまだ使われてないパラメータでなけれ…

「全てのxについてPである。」の反証は、Pでないxを一つ例示すればよい。 「あるxについてPである。(Pであるxが存在する)」の証明は、Pであるxを持って来ればよい。 「全てのxについてPである。」を証明するためには、xが属する集合すべてについて、Pである…

一般に、Aが一つもなければ、命題「全てのAはBである」は必ず真になる。(専門用語では、「空ゆえに真(vacuously true)」という。)驚くかもしれないが、次の命題は真である。 すべてのユニコーンは、五本足である。 この文に反証する唯一の方法は、少なくとも…

全ての人は私の赤ちゃんを愛する。 私の赤ちゃんは私だけを愛する。 ゆえに私は私の赤ちゃんである。はあ？1より、 「全ての人」の中に「私の赤ちゃん」は当然含まれるため、 「私の赤ちゃん」は「私の赤ちゃん」を愛する。そして、 2より、「私の赤ちゃん」…

Print eq. (* ===> Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x *)eq_reflは引数を持たないコンストラクタ。 eq_reflを実行すると、なんらかの型Aの値xを取って、 eq x x (x = x)という命題型の値(つまり証明or根拠)を返す関数？を返す…

式の変形その1 Reserved Notation "e '==>' e'" (at level 50, left associativity). Inductive ReduceNatExpR : Exp -> Exp -> Prop := | R_Plus : forall n1 n2 n3, n1 plus n2 is n3 -> (ExpConst n1) +_ (ExpConst n2) ==> ExpConst n3 | R_Times : fora…

式の定義 Inductive Exp : Type := | ExpConst : nat -> Exp | ExpPlus : Exp -> Exp -> Exp | ExpMult : Exp -> Exp -> Exp. Notation "x '+_' y" := (ExpPlus x y) (at level 50): type_scope. Notation "x '*_' y" := (ExpMult x y) (at level 40): type_…

なんか読書会がもうすぐあって結構な人気らしい。行って覗いてみたい気もするが、すでに定員一杯らしいし、Haskell知らんし、そもそも勉強会読書会なるものについてける気もしないしちょっと無理だろう。件の本は、オンライン演習は一通りやったけど、そうい…

懲りずにソフトウェアの基礎を読み返してるけど、Imp.vあたりから急に難しくなるのはやっぱり気のせいではないと思う。いや、まあそれまでも分からんところはまだ分からんけど。鳩の巣とか回文とか。型付ラムダ計算あたりまでは何とか読みたいところではある…

記号論理の同値関係 「Aであるなら、そのときに限り、B」とかいうやつ。 この字面から、 A B A iff B true true true true false false false true false false false true であることを読みとれとか言われても無理。 包含記号 AならばBってやつね。なんでか…

ざっと読み(解き)終えて思ったこと。超よい本でした。 スマリヤンはやはり手品師です。こんな解った気にさせてくれる本はめったないです。この本で直接書かれてる訳ではないけど、クイズのような問題で手を動かしていると以下のようなことが解ったような感じ…

(define I (lambda (x) x)) (define K (lambda (x) (lambda (y) x))) (define S (lambda (x) (lambda (y) (lambda (z) ((x z) (y z)))))) (define C (lambda (x) (lambda (y) (lambda (z) ((x z) y))))) (define V (lambda (x) (lambda (y) (lambda (z) ((z …

ものまね鳥の本において、算数が出来る鳥(コンビネータ)として以下のものが紹介されてる Vxyz = zxy // λxyz.zxy Ix = x // λx.x fxy = y // KI , λxy.y txy = x // K , λxy.x SUCC = Vf ZERO = I ONE = VfI TWO = Vf(VfI) THREE Vf(Vf(VfI))通常のチャーチ…