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
90 notes, 1 following, 1 followers
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-16 01:51:33)
すでによく本質が理解されているものを再利用するときに高階帰納型はものすごく価値を発揮しそうな感じがする。
自分でうまく定義できる気は正直まったくしない。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-16 00:37:50)
制約が重くなっていくと、目的に対して制約のかけかたが正しい限りは全てがうまくいくけど、正しくできていないと何もかもうまく行かないという印象があるからなあ。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-16 00:34:37)
高階帰納型すごいかもしれない。。。すごい異次元の表現力を見た気がする。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:49:44)
PLFAにでてくる Bin の正規化された構造が自然数と同型な構造のいい具体例なのでちょうどいい。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:48:01)
Agdaの取り組みに戻れるのが最大の回復といっていい。PLFAの1章をCubical Agdaでやってみようと思っていたところで体調不良で倒れていたので、これをやってみる。
本当は1labをしっかり学習した方がいいような気がするけど、なんというか私は暇なので色々勝手に試行錯誤した方が身につきそうでかつ楽しいので。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:38:08)
結構な日数の日記の穴があいたけど、普段の日記の網羅度が高いため、日記が書かれていないという事実がある意味記録になる。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:35:15)
重い体調不良によって、しばらくの間パソコンを開いてタイピングすることすら困難な状態だったのが、今日仕事をしたことでパソコンタイピングに対する壁が無事に消失した
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 12:59:32)
生まれて初めてマクドナルドで野菜ジュース頼んだかも
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 08:44:31)
寒すぎ。。。すごく病み上がりで家を出た選択が誤りだったのではないかと悩ましく思う。引き返して寝たほうがいいのかこれ。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-11 08:41:19)
体温計、ピピピってなったあとに挟み続けているとちゃんとした正確な体温を測れる仕様はちょっと隠し機能すぎる気がする。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-10 11:50:27)
ListとVecは多分特別に難しいから別のにしよう。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-10 00:34:20)
このあと、Listとその長さの依存和とVecが同型であることを示して、同型をパスにして変換できるようにするのをやってみたい
たぶん、Listで定義した非効率で Vec からは定義しにくい rev を Vec から間接的に使えるようになるはず…
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:58:35)
「等しいこと」については「真」か「偽」しかなくて中身がなかった。中身がないから構成する手段もなかった。だから等しさの証明は構成的ではなくて操作的にならざるをえなかった。この問題を解決した Cubical Agda は最強に違いないので色々やってみたいところ。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:44:05)
Agdaだと命題を表現するのに data で型定義をするということがよく行われ、命題の証明は型に対応する証明オブジェクトを構成することによって証明が行うのが自然なアプローチという感じになってる。
しかし、同一性の証明に関しては扱いにギャップがあり sym, cong, subst, rewrite 構文などを使ってうまく命題を操作するプログラムを書く感じになってしまう。
これが Cubical Agda だと、同一性の証明は対応する証明オブジェクト(Path)を構成することになるので、他のアプローチと同じ方法で取り組むことができるのですごい。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:35:45)
「同一性」が第一級のオブジェクトじゃなかったという問題が、HoTTによって解決され Cubical Agda では「同一性」を式の操作ではなく「同一性」を表すデータを構成する形で証明できるようになったというところが嬉しさの核であるように思う。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:47:09)
Agda からrewrite構文と subst が不要になるのは快適すぎる。なんかごちゃごちゃする原因だった。これが Cubical Agda だと lhs と rhs を同時に表す式を書くという考え方になり、これが最強たる所以。これはもう Cubical Agda の前には戻れないかもしれない。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:42:59)
このころだいぶ理解してなかった。Cubical Agdaは等式で式を書き換えようという発想そのものをやめて新しいアプローチに踏み出すやつなので、既存の考え方には全然当てはまらない
https://mastodon.tojo.tokyo/@tojoqk/115862355004663558
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:40:35)
もはや、式を等式で置換するという発想が古いというレベル
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:31:03)
いやまじで Cubical Agda すごいわ。むしろいままでなんでライプニッツの等号で満足していたのかよくわからないレベル。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:29:05)
一回 cong 縛りで List の定理を Cubical Agda で色々証明してみて Cubical Agda のパスの感覚を身体的になじませるか
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:23:52)
こうなってくると結構 Cubical Agda 一択みたいな感じになり普通の Agda に戻る理由はないのでは。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:14:58)
Cubical Agda で Vec の ++-assoc の定義についてどうすればわからなかったので標準ライブラリの答えをみてしまった。
Cubical Agda すごいな。PathP エレガントにインデックス側の +-assoc を処理できてる。これは、 Vec みたいな面倒くさい添え字尽きの依存型を活用するモチベーションがアップするのではないか
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-08 01:25:09)
あー、hcomp のところまで来て自分が Cubical Agda に抱いていたメンタルモデルがかなり間違っていることに気づいた。これパスでつなげるイメージを抱いたから線路的な的なもの組む感じになるのかと思ったけど全然そうじゃなくて高次立方体を構成していくことで等式の連鎖を実現する感じなのか
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-08 00:39:19)
Cubical Agda の勉強中で今日は Partial のあたりを勉強していた。とにかく Cubical Agda は i1 を特別扱いしているということを認識しているところ。。。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-08 00:37:11)
4.4系のままMastodonを最新にした。一応なんか今日はセキュリティアップデートのはずだし早めにということで。
なんかやる気がなかったがそろそろ4.5に上げたいところ。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-07 20:27:38)
ぷよぷよには「なぞぷよ」という詰めぷよぷよが存在するのか。これにACL2を例えるのはかなりいい説明になりそうだけど、自分自身がそんなにぷよぷよ強くない問題があるから、ぷよぷよをやるか。。。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:51:37)
等式に方向があるのはACL2のメリットだと前から思ってはいたんだよなあ
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:26:53)
ACL2で証明した定理をそのまま移植するなら普通のAgdaじゃなくてCubical Agdaのほうが良さそう
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:21:28)
ACL2は、ぷよぷよの連鎖がどこで止まったか教えてくれて連鎖を始める前に戻して何度でも盤面を調整してやり直せるイメージ
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:12:33)
等式を計算とみなす考え方を学ぶ前から既に体得してたの面白すぎるな。
Older Notes