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))通常のチャーチ…

相互再帰を導入した。 ((式1=>SとかKとか) (式2) ...) のような式に対応した。 (use srfi-11) (define (cutlist size car_l result_size l) (if (or (= size 0) (null? l)) (values (reverse car_l) l result_size) (cutlist (- size 1) (cons (car l) car_l…

S (式1) (式2) が S (式1') (式2') (式3) になることはありえない気がする。気がするだけなのが弱い。結局、((式1) (式2) (式3)) みたいなの((式1)を簡約するとSになるようなやつ)には対応せず。つーか (else (map expand-combinator-one seq))を (else (exp…

ラムダ式をSKIコンビネータにバラすプログラムを書いてはみたものの、本当に正しく動いてんのか不安になって、(実際最初は間違ってたし。)逆を行なうプログラムを書いてみた。 (define (construct-S p1 p2 p3 rest) (if (not (pair? p1)) `(,p1 ,p3 ,(if (no…

鳥(コンビネータ)を全て1引数の関数として実装して、schemeで動かそうとすると、どうしても余計に(主観だけど)括弧がついてしまう。 (define I (lambda (x) x)) (define K (lambda (x) (lambda (y) x))) (define T (lambda (x) (lambda (y) (y x)))) (define…

先日のschemeのプログラムは色々間違ってた。x消去で、xを含まない合成手続きXを K X と処理すべきが、 S (K Y) (K Z) になってた。コンビネータとしては冗長だけど、間違ってはいない。といいわけしておく。 ついでにutil.matchを使って書き直してみた。(中…

SKIコンビネータをばらすプログラムをgauche書いた。やっぱものまね鳥の本はすごいと思う。初心者でもこんなことが出来るようになるとは。てゆーかアルゴリズムがまんま書いてくれてあるだけだが。(toSK '(x y) '(x y y)) => (S S (K I)) (toSK '(x y) '(y x…

SICPの遅延評価版schemeで、LによるYコンビネータは上手くいった。 (define L (lambda (x) (lambda (y) (x (y y)))) (define Y (lambda (f) ((L f) (L f)))) ((Y (lambda (f) (lambda (n) (if (= n 1) 1 (+ n (f (- n 1))))))) 10) # => 55 Uコンビネータが…

あいかわらずものまね鳥の本はよー分からんが、Yコンビネータの構成方法は分かった。Lxy = x(yy) という Lコンビネータ(Lark ヒバリ)を使用した Lx(Lx) // x(Lx(Lx)) または以下のチューリングコンビネータを使用した Uxy=y(xxy) UUx // x(UUx) schemeなどの…

ものまね鳥のカリーの森がゲロ吐きそうなレベルで何が書いてあるか分からん。

squid ATSとかvarnishのようなキャッシュサーバって、デフォルトでは不特定多数にキャッシュを消させないようにしてるけど、なんでや？DoS攻撃対策?

デフォルトの設定で、普通に並列に取得してくれた。