title

日々の進捗

関数解析ではルベーグの収束定理の対象を離散的な関数列だけでなく、連続的な関数列まで拡張する命題証明した。少しずつ着実に定義が広がっていく様は過去学習した際には感じとれなかったことだ。

解析教程ではシュワルツの不等式を証明した。2次方程式を利用して証明した。

Common Lisp は (ダグ and Hoyte 2009) を読み初めた。

TaskChuteのログ

本年の目標として数学360時間、コンピュータ360時間を目指す。集計も随時改善していく。

数学の実績時間(今週)
タスク名 実績時間
解析教程の学習 0 days 03:14:00
関数解析の復習 0 days 03:04:00
超幾何関数の論文を読む 0 days 00:19:00
コンピュータの実績時間(今週)
タスク名 実績時間
計量ツールの開発 0 days 02:25:00
Rustのエディター作り 0 days 00:44:00
Common Lispの書籍を読む 0 days 00:16:00
HackerNewsの閲覧 0 days 00:14:00
AWSにログインする 0 days 00:02:00
org-publishの実施 0 days 00:00:00

参考文献

ダグ ホイト, and Doug Hoyte. 2009. Let over Lambda Edition1.0. Translated by タイムインターメディアHOPプロジェクト. 単行本. エスアイビー・アクセス. https://lead.to/amazon/jp/?op=bt&la=ja&key=4434133632.

2025年の環境構築_01

概要

2025年はこのブログにて日々の進捗を詳細に管理できるようにしたいと考えている。まずは以下に取り組む。

  • 日々の学習の寸評
  • TaskChuteのログを一覧にして、作業時間を把握すること

日々の学習の寸評

関数解析ではルベーグの収束定理を学習した。 \varliminf の定義を誤解していたため理解に少し時間がかかった。単関数列で定義した可測関数が可積分関数として定義できたということになるのか。

解析教程では関数解析に出てきたFatouの補題がほぼ同様の表現であった。こちらはリーマン可積分を使っている。並行して2つの内容を学習していたため、このような関係に気づけた。命題の関係性も復習時に考慮にいれてまとめていきたい。

TaskChuteのログ

タスクシュートのログについて で実験した内容を以下のように実行できるようにする。

#+PROPERTY: header-args:python :session (concat "*python* - " (buffer-file-name))
#+PROPERTY: header-args:python+ :var cur_dir=(identity default-directory)
#+PROPERTY: header-args:python+ :eval no-export

#+begin_src elisp :exports none
  (setq-local org-babel-python-command "/home/snowfox/repos/ks_python_env/.venv/bin/python")
  (pyvenv-activate "/home/snowfox/repos/ks_python_env/.venv")
  (org-babel-lob-ingest "taskchute.org")
#+end_src

そして、以下のように実行すればタスクシュートのエクスポート内容を集計可能である。

#+CALL: math_in_thisweek()

以下が出力例になる。

数学の実績時間(今週)
タスク名 実績時間
解析教程の学習 0 days 02:22:00
関数解析の復習 0 days 02:18:00

参考文献

タスクシュートのログについて

タスク管理をTaskChute Cloud 2で行なっている。実績時間を本年の目標に掲げるために、エクスポートしたログを整形するスクリプトを作成した。

今週、今月の数学とコンピュータ関連の作業時間を表で出力できるようになった。

今週

実績時間
タスク名
解析教程の学習 0 days 02:22:00
関数解析の復習 0 days 02:18:00
実績時間
タスク名
HackerNewsの閲覧 0 days 00:09:00
AWSにログインする 0 days 00:01:00
org-publishの実施 0 days 00:00:00

今月

実績時間
タスク名
解析教程の学習 0 days 00:46:00
関数解析の復習 0 days 00:45:00
実績時間
タスク名
HackerNewsの閲覧 0 days 00:03:00
AWSにログインする 0 days 00:01:00
org-publishの実施 0 days 00:00:00

Org2Blogのテスト

本記事はorg2blog の機能のテストを実施している。

以下のように記載するとどうなるか?

#+CATERGORY: TEST1
#+TAGS: TEST2

以下のように TAGS のほうが、WordPressのタグに反映されるようだ。

2024-12-31_13-20-13_screenshot_.png

org2blog-insert-link-to-post連分数の計算 のように投稿へのリンクが挿入できる。

“Dividing unsigned 8-bit numbers”を読んだ

Dividing unsigned 8-bit numbers を読んだ。

  • 除算のSIMD実装を説明している記事である
  • 浮動小数点と筆算での実装をしている

SIMDはやはりよく分からない。また読んでみよう。

備考: 記事内のコードは以下のようにして、 でコンパイルできた。

#include <immintrin.h>
#include <stdint.h>

void avx512_long_div_u8(const uint8_t* A, const uint8_t* B, uint8_t* C, size_t n) {
  // ...
}

“The CAP Theorem of Clustering: Why Every Algorithm Must Sacrifice Something” を読んだ

Why Perfect Clustering Algorithms Don’t Exist を読んだ。

  • 機械学習のクラスタリングのアルゴリズムに関する記事である
  • どんなアルゴリズムにも根本的に欠陥がある
  • 分散システムにはCAPというトレードオフ(両立できない)の関係がある
    • 一貫性(Consistency)、可用性(Availability)、分断耐性(Partition-tolerance)
  • クラスタリングではスケールの不変性、豊富さ、一貫性というトレードオフがある
    • スケールの不変性: データ間の距離を同様なスケールで変えても結果が変わらない
    • 豊富さ: 可能性、グループをどの程度生成できるか
    • 一貫性: 再現性?グループの再編成?
  • Jon Kleinberg は以下の論文で、上記3つの性質のトレードオフを示した

“C++ Is An Absolute Blast”を読んだ

C++ Is An Absolute Blast を読んだ。

  • プログラミング(コーディング)への熱意/興味を記載した記事である
  • 筆者のC++を使用したゲーム開発への取り組みがある
  • プログラミングは業務や組織のために初めたのではない
  • C++がつまらなくなり、今また面白いものになっている
  • 他の言語でもこのような傾向がある
  • C++標準委員会とテンプレートメタプログラミングがつまらなくなった原因
    • C++標準委員会はプログラマの利便を考えなかった
    • テンプレートメタプログラミングを使用するという脅迫観念
  • C++標準委員会は言語を劇的に改善し、面白い言語にした。
  • C++11では auto, nullptr, range-for, lambda expression, などが導入された
  • 標準ではないがファイルシステム、パッケージ管理、グラフィックス、GUIなどが選択できる
  • 言語が人気になるとそれを台無しにする者があらわれる
  • C++は流行遅れになったからよい。
  • C++への不満は
    • エラーの可読性
    • ビルドツール
    • コンパイラーの標準への未対応
    • 歴史が長いことによる複雑性
    • RAII

“How concurrecy works: A visual guide”を読んだ

How concurrecy works: A visual guide | Waqas Younas’ blog を読んだ

  • 並行プログラミングの視覚化により理解を促す記事である
  • 単純な3行のコードを例に用いている
  • 単独プロセスのプログラムの状態を変数の値と実行行番号で表わす
  • 2つのプロセスP,Qのプログラムの状態を変数の値とPの実行行番号、Qの実行行番号であらわす
  • このよう状態空間を定義すると数十プロセスは指数関数的に複雑になる
  • モデルチェッカー(SPINやTLA+)では線形時相論理を利用することができる

“Fermat’s Last Theorem — how it’s going”を読んだ

Fermat’s Last Theorem — how it’s going | Xena を読んだ。

  • フェルマーの最終定理(FLT; Fermat’s Last Theorem)の形式証明を目指している筆者の記事である
  • 形式証明のツールとしては Lean を利用している
  • 対象はアンドリュー・ワイルズが証明した1990年代の証明でなく、クリスタリン・コホモロジーに基づく証明である