読者です 読者をやめる 読者になる 読者になる

きくらげ観察日記

好きなことを、適当に。

Coqのsplit, left, rightについてもう少し詳しく

Coq

inkar-us-i.hatenablog.com上の記事でandを証明するためにsplit, orを証明するためにleft, rightを使えばいいと書きましたが、実はこれらのタクティックはもう少し一般的に作られています。 split splitはandのみではなく、コンストラクタがC : X1 -> X2 -> …

Coqで「任意のxについて…」「あるxが存在して…」を扱う

Coq

Coqで「任意のxについて…」を表すforall xは、xを受け取って残りの命題の証明を返す関数となっています。 Definition prop_1 : forall (x : nat), x = x := fun x => eq_refl x.また、「あるxが存在して…」を表すexists xは、以下のようなデータ型として定義…

Coqで「…かつ…」、「…または…」を扱う

Coq

連言「かつ」、選言「または」を表すandとorは、Coqでは次のようなデータ構造として定義されています。 Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope. Inductive or (A B:Prop) : Prop := | or_in…

Coqで定理の証明中に補題を示す

Coq

assertタクティックを使うと、証明の途中で他の補題を証明できます。 Goal forall P Q R : Prop, P -> (P \/ Q -> R) -> R. Proof. intros P Q R H1 H2. (* H1 : P *) (* H2 : P \/ Q -> R *) (* 先にP -> Rを示す *) assert (P -> R). { (* P -> R の証明 *…

Coqで前提や定理を適用して証明する

Coq

ゴールが前提や既にある定理そのものである場合が、証明の一番簡単なパターンです。 前提がゴールそのものである場合 assumptionを使うと、前提にあるゴールと全く同じ命題をそのまま適用してくれます。 Goal forall P : Prop, P -> P. Proof. intros. (* P …

Coqで数学的帰納法を行う

Coq

数学的帰納法を行いたい場合は、基本的にelimかinductionのどちらかのタクティックを利用します。 elim こちらが最も基本的な帰納法です。elim x.とすることで、xについての帰納法を行うことができます。 例えば、以下のコードでは直接to_zero n = 0を示すの…

Coqでデータ型に対して条件分岐を行う

Coq

証明中にデータ型に対して条件分岐を行うためには、case, case_eq, destruct等を使います。 とりあえず普通に条件分岐をする caseは普通の条件分岐です。例えばb : boolに対してcase b.とすると、b = trueである場合とb = falseである場合の2つに分かれ、そ…

Coqで定理の特定の項だけを書き換える

Coq

rewriteやsimplを使って定理を書き換えようとすると、どうしても思ったとおりに書き換えがいかないことがあります。 (* 結合法則と交換法則を使って、3つの項を入れ替える *) Goal forall (T : Type) (op : T -> T -> T), (forall x y z : T, op (op x y) z …

Coqで既存の定理、定義に従って計算する。

Coq

定義に従って計算する 定義に従って計算するには、simpl, compute, unfoldが使えます。 simpl.はゴールの式をいい感じに簡単にしてくれるのに対し、compute.はとりあえず式展開します。また、unfoldは定義の左辺から右辺に書き換えます。 Fixpoint fact (n :…

Coqで前提の矛盾から定理を証明する

Coq

矛盾を導く方法は何通りかあります。 すでに前提にFalseがある場合。 まずは一番基本的な方法から。既に前提にFalseがある場合です。 Falseの定義は、以下のようになっています。 Inductive False := (* コンストラクタが1つもない *).従って、前提にP : Fal…

Gaucheで文字列のシーケンシャルアクセス

Gaucheでそこそこサイズの大きい文字列へのシーケンシャルアクセスをしたい場合の注意点です。例として、以下のURLにある『吾輩は猫である』の文書中に、何回「猫」という文字が出てくるかを調べてみましょう。http://www.aozora.gr.jp/cards/000148/card789…

Gaucheでロード時定数を作る

Gaucheには元々ロード時定数という機能はありませんが、マクロを使ってうまいこと頑張ると作ることができます。 ;; ロード時定数を保存するためのモジュール (define-module *constant-table*) ;; モジュール module の中で expr を評価し、 *constant-table…

Basic認証の方法を理解する

Basic認証は数あるHTTPの認証方法の中でも最も簡単なものです。認証方法は、ユーザー名とパスワードをコロンで繋いだものをbase64でエンコードし、Authorizationヘッダの値に"Basic (先ほど作った文字列)"をセットするだけです。アホみたいに簡単なので、不…

Gaucheでクラスのフィールド名を変数に束縛する。

HaskellでいうNamedFieldPunsのようなものです。 クラスのインスタンスと、スロット名のリストを渡すことによって、スロット名と同名の変数にスロットの値を束縛するマクロを書きました。使用例は記事の下の方にあります。 ;; macro let-slots (((slot-name …

Schemeと各括弧

多くのScheme処理系では、角括弧[]が通常の括弧()と同一視されます。 この角括弧の使いどころについてまとめてみました。 角括弧は使うな まず始めに結論から書くと、今後書くSchemeのコードでは、角括弧は使用しない方が良いでしょう。というのも、R7RS*1に…

Gaucheでソースコードのあるパスを取得

きちんと ./configure && make && make install するようなプログラムでもない限り、ソースコードを適当にどこかから引っ張ってきて、そこから $ gosh ./main.scm するだけでとりあえず動くようにできたほうが楽な場合はよくあります。 しかし、Gaucheでそれ…

Gaucheで#<eof>を返す

ジェネレーターを自作する場合なんかに#<eof>を返したくなる場合がありますが、以外とググッても方法が出てきません。R6RSの(eof-object)を使えば簡単に生成できます。 ;; 1からnまでの数を返すgeneratorを返す (define (gen n) (define i 0) (^() (if (<= n i) (</eof>…

Schemeにおける「多値」という概念について

inkar-us-i.hatenablog.comこの記事で少しだけ多値について紹介しましたが、この頃はまだよく存在意義がわかっていませんでした。 そもそも多値とは? 大雑把に説明すると、valuesとかhoge&fuga関数を呼んだ時に値が複数返ってくるアレです。 (values 3 2 1)…

Gaucheで値の比較

値の比較に使用する関数は通常eq?, eqv?, equal?の3種類あるのですが、それらの使い分けが曖昧だったのでまとめてみました。 eq? (eq? x y) はxとyが全く同じオブジェクトであるか(=メモリ上の同じ位置にあるか)どうかを判定します。Pythonのisに近いやつで…

Gaucheでデバッグ

Gauche Users’ Reference: Top上のサイトを見る限り、printfデバッグ的なことをするためには#?= #?,の2つの構文が使えるようです。とりあえず#?=の使用例。 gosh> (define (foo x) (+ x 1)) foo gosh> #?=(foo 3) #?="(standard input)":21:(foo 3) #?- 4 4 …

Gaucheでreturn文

return文のようなものは比較的簡単に作れますが、念の為覚え書き。値を返したい位置の継続を受け取って、returnするかわりにその継続に戻り値を渡します。 (use gauche.collection) ;; xsとysのすべての要素が等しければ#t, そうでなければ#f (define (vecto…

coq-modeとproofgeneralでcoq環境を作る

Coq

EmacsでCoqを扱う場合、proofgeneralというものを使うのが一般的らしいです。 $ sudo apt-get install coq proofgeneral Ubuntuの場合はどちらもaptのリポジトリに入っているので、上のコマンドを打つだけでインストールは完了です。 (load-file "/usr/share…

Gaucheに継続を「実装」する

http://inkar-us-i.hatenablog.com/entry/2016/09/01/200000inkar-us-i.hatenablog.com上の記事でしっかりしたモナドが作れたので、これを使って継続を実装します。 (define (cont-return x) (^(cont) (cont x))) (define (cont-bind x f) (^(cont) (x (^(xv…

Gaucheでモナド その3

http://inkar-us-i.hatenablog.com/entry/2016/08/27/200000inkar-us-i.hatenablog.com上の記事で作ったモナドはグローバルなスタックに現在のモナドを積むというものでしたので、mlet*の終了と同時に現在使用しているモナドに関する情報が消滅してしまい、…

libraryとexecutable両方を含むcabalパッケージを作る

cabal initした時に「libraryとexecutable、どっちのパッケージにする?」みたいなことを聞かれるので、今まで1つのパッケージにはlibraryとexecutableのどちらか一方しか含むことができないと思っていました。.cabalにlibrary:とexecutable:の両方を書けば…

Pythonにおける弱参照

Pythonにも弱参照は存在するらしく、weakrefというモジュールで提供されています。 >>> import weakref >>> class A(object): pass ... >>> a = A() # ... (*) >>> ptr = weakref.ref(a) >>> ptr() <__main__.A object at 0x7fd47bb929b0> >>> del a ... (しばらく色々な操作をして、GCが呼ばれる</__main__.a>…

stackでプロファイリングを有効にしてビルドする

以下のようにオプションを渡せば、stackでもプロファイリングを有効にしてビルドすることができます。 $ stack build --executable-profiling --library-profiling --ghc-options="-fprof-auto -rtsopts" あと、実行時にも1つハマりどころがあります。ビルド…

ようやくstackを使い始めた話

レポートの提出期限間際にcabalの依存関係がぶっ壊れて大変な思いをしたので、ようやく重い腰を上げてstackを使い始めてみることにしました。 インストール インストール方法とかはだいたいこの辺を参照しました。stack/install_and_upgrade.md at master · …

Gaucheでモナド その2

inkar-us-i.hatenablog.comこのときはGauche歴半日くらいだったんで中置演算子とか定義してて微妙な感じの構文だったので、もう少しLispらしいモナドを書いてみました。 (define *monad-stack* '()) (define (push-monad! monad) (set! *monad-stack* (cons …

Emacs Lispにおける関数の扱い

他の人のEmacs Lispの設定を眺めていて気づいたのですが、(add-hook hoge-hook XXXX)のXXXX部分にlambdaを入れる場合、 (lambda () ...) と普通に書く人と、 '(lambda () ...) みたいにクオートして書く人と、 #'(lambda () ...) みたいな謎クオートする人が…

CPSとSSA

SSA(Static Single Assignment form, 静的単一代入)とは、一つの変数についての代入文がプログラム中で一度しか現れないような書き方のことを指します。 Scalaでいうと、すべての変数がvalになっているようなものですね。プログラムをこの形式に変換すること…

CPS変換についての覚え書き

CPS(継続渡しスタイル)とは、関数自体に「その後の処理」を引数として渡してしまうような書き方です。例: ;; 点(x . y)のノルムを求める (define (norm x y) (sqrt (+ (expt x 2) (expt y 2)))) (norm 1 1) ; => 1.414... ;; normのcps版 (define (norm/cps …

Ook!はSchemeである

Ook!のソースも、括弧で括ればただのS式ですよね。 ;; ook.scm (define *mem-size* 10000) (define *mem* (make-vector *mem-size* 0)) (define *ptr* 0) (define (inc-ptr!) (inc! *ptr*)) (define (dec-ptr!) (dec! *ptr*)) (define (inc-mem!) (inc! (~ *…

Gaucheのコメントいろいろ

なんか今更な気もしますが……。 行コメント セミコロン(;)から行末まではコメントとみなされます。セミコロンの数にも作法があるみたいです。 ;;; モジュール自体の説明とか、大きなコードブロックの説明 ;;; ;;; このモジュールはフィボナッチ数を生成するジ…

multi-termで快適なキー操作

multi-termで作業してると、「単にシェルとして扱いたい場合」と「シェルの出力を編集したい場合」とでほしいキーバインドが異なる場合があります。例えば、C-aにterm-send-rawを割り当てているとして、普通にコマンドを打っているとき $ sl ./hoge/fuga/fo#…

dynamic-wind

R5RSではdynamic-windという面白い関数が定義されています。 (dynamic-wind before thunk after) dynamic-windはまずbeforeを呼び出し、その次にthunkを、最後にafterを呼び出します。試しに以下のようなプログラムを実行してみましょう。 (define *outer-co…

Gaucheの複素数

gosh> 1+3i 1.0+3.0i gosh> i *** ERROR: unbound variable: i gosh> 2i *** ERROR: unbound variable: |2i| この書き方キモくないですか?複素数なんて特定の用途にしか使わないし、別に複素数リテラルとか用意しなくても gosh> (complex 3 5) 3.0+5.0i み…

Gaucheで手続き以外のオブジェクトも呼び出し可能にする

object-applyというメソッドを定義すると、手続き以外の任意のデータ型をあたかも関数であるかのように呼び出すことができます。 ;; (数 数)を(* 数 数)にする (define-method object-apply ((x <number>) (y <number>)) (* x y)) (define x 5) (3 x) ; => 15 以前説明したパ</number></number>…

Gaucheでパラメータを定義する

Gaucheには、グローバル変数の代わりに使用できるパラメータというオブジェクトが存在します。 パラメータの作成 (define x (make-parameter 3)) (x) ; => 3 (x 100) ; xの値を100に設定 (x) ; => 100 典型的な使い方としては、特定の関数が使用するデフォル…

Gaucheで優先度付きキュー

Gaucheの練習。実は何気に優先度付きキューの実装は初めてだったので、ツリーを配列で管理したほうが楽ということを知らずに若干手こずりました。 (define-class <priority-queue> () ((queue-vector :init-keyword :queue-vector :accessor queue-vector) (size :init-keywo</priority-queue>…

Gaucheでリスト内包表記

srfi-42には、リスト内包表記に関するマクロが定義されています。 (use srfi-42) ;; Haskellでいう ;; [i * 2 | i <- [0, 1, 2, 3, 4]] (list-ec (: i '(0 1 2 3 4)) (* i 2)) ; => (0 2 4 6 8) ;; iの値の範囲の指定もできる (list-ec (: i 0 5) (* i 2)) ;…

パターンマッチでTextを1文字ずつ処理する

PatternSynonymsのいい感じの実用例が思いついたので。 {-# LANGUAGE PatternSynonyms, OverloadedStrings, ViewPatterns #-} import Data.Text pattern c :+ cs <- (uncons -> Just (c, cs)) このパターンを定義することで、先頭文字がcで残りがcsであるよ…

Gaucheで構造体を定義する

クラスほど大したことをしなくても良い場合、define-record-typeというマクロを使うことでより簡単な構造体を定義することができます。 (define-record-type point #t #t x y) (define p (make-point 3 4)) (point? p) ; => #t (point-x p) ; => 3 (point-y …

Gaucheで関数の実行時間を測定する

gauche.timeのtime-this関数を使うと、指定した関数の実行にどれくらい時間がかかるのかを測定することができます。 (time-this 実行回数 実行する関数) 例として、クラスを使った場合と、ベクタを適当にラップした型に対してアクセスするのとで、どの程度実…

Pythonで代数的データ型とパターンマッチ

PythonでHaskellっぽい代数的データ型とパターンマッチをできるようにするためのメタクラスです。 まあこれも余り用途はなさそうですけど。 def AlgTypeMeta(*names): class _AlgTypeMeta(type): def __new__(metacls, name, bases, methods): def init(self…

Pythonでsealedクラス

とくに意味も用途もないけど何となく思いついたので作ってみました。sealedクラスとはScalaの機能で、別モジュールからの継承をできなくさせる機能です。 # sealed.py class SealedException(Exception): pass class SealedMeta(type): def __init__(self, n…

Gaucheで多値を受け取る

複数の値を返す場合、それらの値をリストやペアにしてもよいのですが、通常、Schemeでは多値というものを利用します。 gosh> (min&max 2 4 3 1 5) 1 5 このmin&maxは、与えられた引数のうち最小値と最大値を返す多値関数です。他にも、商と余りを返すquotien…

ImplicitParamをConstraintとして扱う

=>の左側に来るものはすべてConstraintなので、暗黙引数をConstraintとして扱うこともできます。 {-# LANGUAGE ConstraintKinds, ImplicitParams #-} type Showable t = ?show :: t -> String print' :: Showable t => t -> IO () print' a = putStrLn $ ?sh…

Gaucheでデータ型の簡単な表現を定義する

例として、以下のようなクラスを用意します。 (define-class <person> () ((name :init-keyword :name) (age :init-keyword :age) (pref :init-keyword :pref))) このようなクラスのインスタンスを作成してみます。 (define taro (make <person> :name "Taro" :age 20 :pref </person></person>…

Cabalで静的ファイルをパッケージに含める

YourPackage.cabalに data-dir: dirname data-files: *.txt img/*.pngのように記述すると、dirname以下のdata-filesに指定したファイルがインストール時にコピーされます。また、これらのファイルにアクセスするためのPaths_YourPackage という名前のモジュ…