hatsugai is a user on mathtod.online. You can follow them or interact with them if you have an account anywhere in the fediverse. If you don't, you can sign up here.

hatsugai @hatsugai@mathtod.online

式しか書いてなかったけど,問題文も Twitter から転載,編集.

------
証明クラスタへ楽しめる問題を紹介(再).自然数 $M > 0$ を固定.$M$ 未満の自然数からなるリストは次の関数 $\mathrm{enc}$ で自然数にエンコードできる.1. 自然数をリストにデコードする関数 $\mathrm{dec}(n) $を定義,2. $\mathrm{dec}(\mathrm{enc}(s)) = s$ を証明, 3. $\mathrm{enc}(\mathrm{dec}(n)) = n$ を証明.

ここで $\langle x \ldots \rangle$ はリスト,$s^\frown t$ はリストの連結とする.

$$\begin{split}
& \mathrm{enc}(\langle \rangle) &= 0 \\
& \mathrm{enc}(\langle x \rangle^\frown s) &= 1 + x + M \mathrm{enc}(s)
\end{split}$$

$$\begin{split}
& \mathrm{enc}(\langle \rangle) &= 0 \\
& \mathrm{enc}(\langle x \rangle^\frown s) &= 1 + x + M \mathrm{enc}(s)
\end{split}$$

高校生のときに数学の先生に教えてもらった問題を形式化したくて,ときどき思い出しては考えるのだけれど,いまだにできない.かんたんに形式化できる問題とは何か違うってことだろうから,きっと何か得られると期待している.

物理系の友人が、物理学者にはランダウ型とファインマン型がいるとかなんとかいってた。全員天才かよとか思った(小並)。

Coq 二日間集中か。すごいな。使えるようになるんだろうか?

CONCRETE MATHEMATICS 読みたくなってきた...

あーあ,そんな贅沢な時間があればなあ...

数列を差分の形に書き換えて和をとる変形が楽しい.高校生のとき,先生が具体的に項を書きだして丁寧に説明してくれたことを思い出す.

$$a_{k+1} - a_k = c_k \quad (k \ge 0)$$

これを $k=0$ から $n$ まで辺々足すと

$$a_{n+1} - a_0 = \sum_{k=0}^n c_k \quad (n \ge 0)$$

定数係数の3項間漸化式で特性方程式が重解を持つとき、$\lambda^n$ の他に $n \lambda ^n$ や $n$ の2次式が解になるしくみが高校生のときはわからなかったけど、いまさらながらわかった。ちょっとうれしい。そういえばこのあたりは秋山仁さんに習ったのだった。

SMT solver Z3 を使ったテストケースの自動生成器を作ってみた.

qiita.com/hatsugai/items/66631

SMT solver Z3 を使ったプログラムの正当性検査器を作ってみた。

qiita.com/hatsugai/items/cf89a

資料用にてきとーなシミュレーションを書いて遊んでいた.もっと涼しげなものがよかったか mathtod.online/media/NPy7VQzx9

拡張ユークリッドの互除法を復習した.

定義は $ N \triangleq E $ を使う.