ushumpei’s blog

生活で気になったことを随時調べて書いていきます。

Lean4 でゲーム理論

MixedMatched/formalizing-game-theory というリポジトリでゲーム理論を Lean4 で形式化している人がいて、自分がやりたかったことはこうやればいいのか、と勉強になった。読んだ内容をメモとしてまとめておく、ファイルはこれ: https://github.com/MixedMat…

Lean4 学習10

Lean4 を数学の証明以外で使ってみたい気持ちがあり、しかし現実にある複雑なプログラムを検証する方法がわかっていないため、とりあえず FizzBuzz の証明を書いてみました。 import Std def fizz_buzz : Nat → String := fun n => if n % 15 = 0 then "Fizz…

Lean4 学習9'

Lean4 学習9 - ushumpei’s blog こちらで定義した range' : (n : Nat) → Vector (Fin n) n という関数、もっと簡単に定義できた。 range を定義してから型の対応関係を考えるというのが逆で、型の対応関係を考えたら自然と range に相当するものが出てきた感…

Lean4 学習9

Lean4 で有限個の要素をいい感じに扱いたくてどうすればいいか悩んでいて、Fin n → α がそれに当たるかなーとか考えたのですが、プログラミングにおいては Vector α n (長さ固定の List α) が使いやすいのでその間を埋めることができないかなと色々していま…

Lean4 学習8

Lean4 で証明とプログラムをうまく組み合わせたものが書けないか色々試している。証明を書いて、その具体的な値を使って何かするといったことがなかなかうまく出来ず、何となくこれでいいんじゃないかな、という方法が少しわかったのでメモしておく。単体を…

モナドは自己関手の圏 (で自然変換を射、関手の合成を演算と見た場合) におけるモノイド対象

概要 自然変換の垂直合成、関手との合成がわかった結果 モナドは自己関手の圏 (で自然変換を射、関手の合成を演算と見た場合) におけるモノイド対象 だと言葉の意味を理解した。「自己関手の圏って言ったら射、演算は決まりきっているだろう」と言われたらそ…

Lean4 学習7

ヤングアニマル Web に数学ゴールデンがあった (https://younganimal.com/series/a2c408d4be5da/) ので読んだら鳩の巣原理が出てきて、証明できそうだったのでやってみた。有限集合の濃度の不等号を仮定に単射が存在しないことを示す方針、本質は単射から濃…

Lean4 学習6

パターンマッチを書いている時、 match xs with | [] => [] | y::ys => _ としたときに二番目にマッチしたケースでは 0 < xs.length が成り立っていて欲しいけどそれはダメみたい?そう言う場合はどうすればいいか?素直に if h : 0 < xs.length then ... el…

Lean4 学習5

Inductive Types の Exercises の exponentiation の実装。 色々感じが掴めてきて rw、simp を使わないでかけるようになってきた Eq.refl に何か渡すことで 何か = 何かの評価 の等式が得られる Eq.refl は自動的に解決されるので calc の Eq.refl の行は本…

Lean4 学習4

n 番目の fibonacci 数を求める 2 つの関数が等しいこと (全ての引数に対し等しい戻り値を返すか) を証明してみた。 まず fib1 は素朴な実装 open Nat def fib1 (n : Nat) := match n with | 0 => 0 | 1 => 1 | n + 2 => fib1 n + fib1 (n + 1) #eval fib1 1…

lake のパッケージの置き方

Lean4 では lake コマンドを使用してプロジェクトを作成する、作成したプロジェクトでパッケージの整理をする際に、少し詰まったのでメモしておく。結論はプロジェクト名のディレクトリを作成してそこにファイルを作るとインポートできる。 lake init を使用…

Lean4 学習3

Quantifiers and Equality の演習にて、床屋のパラドックスを示す問題があった。これは排中律を使用すればすぐに解けるのだが、検索してみると構成的証明があるとのことで、やってみると解けた。 variable (men : Type) (barber : men) variable (shaves : m…

Lean4 学習2

Quantifiers and Equality の The Existential Quantifier セクションにある問題を解いた。 変数名を気にして書いてみたけど一向に読みやすくならない、たとえばこんなやつ (シンタックスハイライトないのでさらに読みにくい) example : (¬ ∀ x, p x) ↔ (∃ x…

Lean4 学習

Lean が気になっているので Theorem Proving in Lean 4 の Propositions and Proofs にある演習問題を解いた。プログラムによる定理証明に触れるのは初なので、時々型を定理だと認識できなくなって迷走してしまうなど苦労した。 Lean4 が気になっている理由…

Litestream 入りの Dockerfile 作る

Litestream を Dockerfile に同梱して node のなんか動かすやつです。ここでは Next.js & Prisma 構成のサーバー動かします。 主な必要なファイル Dockerfile litestream.yml entrypoint.sh 1. Dockerfile FROM node:18-alpine as builder ADD . /app WORKDI…

serverless の設定で簡単なロジックを含める

stage とかに応じて設定を変える方法があったのでいじってみます、${opt:stage} とかよりもっと複雑なことしたくなったときに使えると思います: https://www.serverless.com/framework/docs/providers/aws/guide/variables/#exporting-a-function なんとなく…

javascript の ArrayBuffer

なんとなく javascript の ArrayBuffer 触っている。データをストリームで処理することが自分は好きなのかもしれないって最近思って、テキストは特にすることがないのでバイトデータ、という感じで。 とりあえず jpeg からサイズ情報が取れる程度のパーサー…

Deno で簡単な重複行削除スクリプトを書いた

ファイルの重複行削除がしたかったのでスクリプトを書こうと思ったのですが、せっかくだし Deno で書いてみることにしました。 https://github.com/ushumpei/scripts/blob/main/remove_duplicate_lines.ts import { iter } from "https://deno.land/std@0.93…

WordPress で独自の rss フィードを設定する

意外に簡単だったけど忘れそうなのでメモ。 functions.php に以下を記述

Java でストリームの末尾数行を捨てる

末尾の行を捨てるためには一旦ファイルを全部読まなきゃいけないかと思ったけど、捨てたい行数を先読みしておけば良いという感じでした。 import java.io.*; import java.util.LinkedList; import java.util.Queue; // ファイルの末尾数行捨てる BufferedRea…

WordPress のテーマで、依存している Plugin をインストールしてもらう

必要な plugin がある場合に、通知を表示してインストールしてもらう class 作る (名前空間としてだけ使っている、作法はわかっていない) functions.php で require_once して呼び出す コード required_plugins.php

Vue.js の slot と props

内容としては これ (Vue.js のガイドの「スロット」の「スコープ付きスロット」) を読んで理解できなかった自分向けのメモです。 Vue.js で slot を使ったコンポーネントの持つ値を、slot に差し込まれるコンポーネントに props として渡す方法を調べました…

Node.js の stream.pipe のエラーハンドリング

stream.pipe の代わりにバージョン 10 で追加された stream.pipeline を使うと良さそうです。 stream.pipe では ここ に書かれているように、エラーハンドリングとしてストリームの後始末を書かなければいけないためです。 One important caveat is that if …

Node.js でオブジェクトの配列からストリームを作成する

多分知っておくべきこととして、ストリームはバージョン 12.3.0 でかなり変化があった。この記事は 11.15.0 で書いている。 Node でオブジェクトの配列からストリームを作る方法。 const { Readable } = require("stream"); const readable = Readable.from(…

GZIPOutputStream と ByteArrayOutputStream と try with resources

Java の try with resources は途中で return してもリソースの close をしてくれるけど、なんか間違えた。 GZIPOutputStream と ByteArrayOutputStream を使って以下のような、データを圧縮してバイト列にして返す処理を書いていました。( InputStream の部…

修了証明書

Certificate of Completion スライドとかでよかった気がするけど、なんとなく html で修了証明書を書いてみました。css は無限に時間を溶かすと思います。 See the Pen Certificate of Completion by ushumpei (@ushumpei) on CodePen. Mac の Chrome でしか…

VSCode で Ruby 書くための設定

PC 変えた時に vim & ruby のいい感じの設定が失われてしまいしばらく書かないから放置していたらまた書くことになり VSCode でなんとなく書いてたらいい加減不便さを感じてきたので本当にとりあえずの設定を調べました。(早口) この辺ができるように設定。 …

open-uri の close とか

ruby の open-uri の open で、サイトをスクレイピングするプログラムを見かけたのだけれど、「close 呼ばなくていいの?」と思って色々調べたのでメモしておきます。結論としては、ブロック渡した時は呼ばなくていいけど基本的には呼ぶ。 調べたのは ruby 2…

静的 html を BASIC 認証付きで雑に公開する方法

雑なメモです (なんかやばかったら教えていただきたいです) 1. 適当なリポジトリを作成する $ mkdir private $ cd private $ git init 2. html ファイルとかを配置する $ echo '<html><head><title>private</title></head><body><h1>I am private!</h1></body></html>' > index.html 3. heroku アプリを作成して、 php のビル…

PostgreSQL 10 でパーティションをまるっと切り替えてみる

PostgreSQL の 10 では宣言的パーティショニングが使えるようになったそうですね (しかし僕は 10 以前でパーティショニングしたことがなかったので感想がない) これを使ってデータの一括削除、一括追加を実現するために、パーティションの切り替えについて練…