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
190 notes, 1 following, 1 followers
きゅーけー@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)
等式を計算とみなす考え方を学ぶ前から既に体得してたの面白すぎるな。
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に取り組むべきであるという根拠がまた増えてしまった感…
Older Notes