Home | Notifications | New Note | Local | Federated | Search | Logout
きゅーけー@tojoqk@mastodon.tojo.tokyo
Lisp と自由ソフトウェアと行動分析学が好きです。
自分専用のマストドンサーバーを運用しています。
Typed Racket や Coalton のような型のついている Lisp や、定理支援系の Agda、GNU Guix System に興味があります。
いまは Agda 学習がメインです。
生活リズムの安定のため、深夜 02:00 から 10:00 までの間はアカウントロックをかけています。その間は何も反応しません。
個人サイト: https://www.tojo.tokyo
サブアカウント: https://fedibird.com/@tojoqk
Joined: 2025-12-01 20:07:27
92 notes, 1 following, 1 followers
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:12:33)
等式を計算とみなす考え方を学ぶ前から既に体得してたの面白すぎるな。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 21:39:37)
これは完全にトレードオフだな。危険だけど大連鎖の爽快感を楽しみたいなら ACL2 のほうがいいけど、緻密にかつ安全に進みたいなら Cubical Agda のほうが良いという感じ。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 21:27:36)
ACL2の記事書くならCubical Agdaをやってからのほうが良さそうだな。まだ理解に自信はないけど、おそらくACL2はぷよぷよで大連鎖を起こすようなスタイルで、Cubical Agdaは電車の線路を引くような感じで明示的に安全性が保証された連鎖を記述する感じなんだと思う。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 21:01:11)
ACL2をヒューリスティックから型理論に昇華したもののような気がしてきた。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:57:09)
Cubical Agda、もしかしてACL2で身につけた感覚がとても役に立つものなのでは…？
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:27:22)
guixとnixの両方が入ったFedoraになってしまうな。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:26:54)
1labのためにnixのインストールが必要らしく流石にこれは自宅で実行したほうがよさそうな感じだな。。。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 20:08:37)
1labのドキュメントを読んでいくのが良さそうな雰囲気らしい
https://1lab.dev/
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 19:40:39)
これからはCubical Agdaの学習に集中したいと思う。学習する価値が極めて高い気がする。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 14:32:56)
Cubical Agdaに取り組むべきであるという根拠がまた増えてしまった感…
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 14:13:45)
数学基礎論と物理学を組み合わせる研究はすでに進んでいて、小澤正直教授によって劇的に進展していたということを知った。数学基礎論って物理学にも応用されてたのか。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 09:30:49)
AgdaとACL2を趣味で触っていた結果、数学基礎論的な思想に間接的に触れることになり、物理学の統一理論が「存在する」ということについての非自明性に気づくように導かれた感じがある。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 08:49:06)
そもそも数学的に両立可能なのか疑問に思い始めてから、子供の頃からなんとなくあった統一理論への憧れ、超ひも理論への興味みたいなことが急速に崩れていくような感覚がある。同時に自分にはプラグマティズム的な感覚もあって、そもそも観測できない領域について論じる物理学って本当に必要なのだろうかということも考え始めるようになっていっている…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 08:26:38)
理論物理学について、マクロの世界を記述する理論とミクロの世界を記述する理論と組み合わせた統一理論を作るという話があるけど、そもそもマクロの世界とミクロの世界を同時に表現できる体系というものが存在するかどうかって自明ではないのではないかということに気づいた。同時に成立しないことが数学的に証明できる可能性すらあるのではないか…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 22:15:48)
ACL2は一見一回論理に限定されている分簡単そうに見えて、実際のところはバリバリ古典AIの究極成果みたいな感じで、ヒューリスティック探索のコツを掴んでいくことこそが大切だったりすることが難しい。
あと、ガードの話は書かないと静的型付け全盛期の今の時代いけない気がするものの、ガードがACL2のロジックに影響しせず、ガードはほかのガードとのみ影響し合うといったところは明らかに簡単に説明できるものではなく公式ドキュメントを読もうとなってしまうあたり大変…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 22:12:04)
ACL2の記事執筆、あまりにも難産すぎて苦しくなってきたので一旦置いておくことにした。。。
そもそもむずすぎるし、書いていると無限に改善点が見つかる。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@qnighy@qnmd.info (2026-01-05 22:00:32)
もしイベントを外部のアクターに処理させたければ、まず変更と同じトランザクションで(同じデータベースに)キュー要素を積み、それをワーカーが取り出して外部用のメッセージキューに投げ直すといった方法は考えられる
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@qnighy@qnmd.info (2026-01-05 22:06:17)
非同期処理のキューの場合結果整合性で済ますが前提なので絶対にトランザクショナルじゃないといけないわけではないが、メッセージ喪失の対策だけでも意外と大変なので最初からトランザクショナルにすればいいのに……という意図
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 22:07:13)
トランザクションの処理はRDBの中で完結させないとおかしくなるんだよな…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 22:00:18)
たしかに…、RDBでエンキューまで全て済ませるのはだいぶ正解感があるな…
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@qnighy@qnmd.info (2026-01-05 21:56:38)
@anqou ぼくの投稿は「同じデータベース内に」と書きました
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:48:29)
まさかスマホとここまで密結合したデバイスだとは…
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:47:08)
そもそもスマートウォッチの実態をよく知らずに買っちゃったところから始まってるからなあ
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:46:20)
GadgetBridgeのおかげでプライベートな生活情報をクラウド管理されることなく便利機能を享受できるようになっているので、GadgetBridgeがなかったらと思うと困る…
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-05 21:42:51)
GadgetBridgeはとてもいいものではあるが、デバイスを購入した時点で、プロプライエタリなソフトウェアを前提とする販売元に利益供与しちゃう問題はあるよなあ…。Windowsの入ったノートパソコンを買ってその後にWindowsを消しているものの買ったときにWindowsに貢献してしまうとの同じ問題がある。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@boronology@social.penguinability.net (2026-01-05 21:31:33)
私は自分の理想が全体にとって最適な自信なんてこれっぽっちも持ってないので「自分向き」という表現をしていますが、信じる正義のある人は「良いもの」に読み替えていただければと思います
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@boronology@social.penguinability.net (2026-01-05 21:26:20)
ない、んだが。それはともかくとして人々はもう少し自分の行住坐臥に政治的な意味合いをも持たせうるのだということを知ってほしいとは思う。ものを買うときにはある種のものを選ばないだとか、道具を選ぶときにある種の属性に価値を見出すとか、そういう判断の一つ一つが将来の状態をより自分向きにしていくための一助となるということ。
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@boronology@social.penguinability.net (2026-01-05 21:16:16)
私は常にプロプラなものの提供者を脅迫し続けるつもりでいるけど、そこまでの先鋭さを全員に求めは（あまり）しない
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@boronology@social.penguinability.net (2026-01-05 21:11:23)
これ私の方向性と割と近い。プロプラなものがあることと、そのメリットの存在を認めながらも常に代替の存在を確保し続けること自体が将来的な価値を増加させると思っている
きゅーけー@tojoqk@mastodon.tojo.tokyo boosted:
@anqou@mstdn.anqou.net (2026-01-05 21:26:32)
多分単純な解は無いので問題に応じてうまくやる必要があるんだと思っている
Older Notes