core.lean 内の定義： @[inline] def band : bool → bool → bool | ff _ := ff | tt ff := ff | tt tt := tt notation x && y := band x y[inline] というアトリビュートがある。その場で展開されるのかな？アンダスコアは無名変数〈匿名変数〉で、パターン…

ハブは： https://leanprover.github.io/documentation/ → Lean4のマニュアル作業中、現状は参考になっても参照はしないだろう。 → Learning Lean すぐ下 https://leanprover-community.github.io/learn.html https://leanprover.github.io/publications/ ht…

検索文字列"from:m_hiyama leanprover"で、Twitter検索をすればいい。 https​:​//twitter.com/search?q=from%3Am_hiyama%20leanprover&src=typed_query

Haskellで「アクション」という言い方があるが、どうもクライスリ射のことらしい。IOアクションは、IOモナドのクライスリ射という具合に。となると、Leanのtacticモナドのクライスリ射はtacticアクションとなるが、「tacticアクション＝タクティク」だから、…

import system.io #eval io.print_ln "hello world"try it!

privateな名前は、名前空間の内部しか使用できない。外部からのアクセスが禁止される。protectedな名前は、アクセスは可能だが、openして外部にばらまくことができない。 private -- 外部からのアクセスは不可能。 protected -- 接頭辞付きでならアクセス可…

以下は、$USERPROFILE/.elan/toolchains/stable/bin/leanpkg.bat @ECHO OFF SET LEANDIR=%~dp0%../ SET LIBDIR=%LEANDIR%\lib\lean IF NOT EXIST "%LIBDIR%" SET LIBDIR=%LEANDIR% SET LEAN_PATH=%LIBDIR%\library;%LIBDIR%\leanpkg SET PATH=%LEANDIR%\bin;…

inductive foo : Type := | bar : foo | baz : foo と書きたくなるが、:= は要らない。なぜなのだろう？[追記]match/with/end の省略と同じみたいだ。[/追記]

section funcomp variables {X Y Z:Type} def comp (f:X → Y) (g:Y → Z) :X → Z := λ x:X, g (f x) end funcomp #check comp infix `;` := comp constants A B C D:Type constants (f:A → B) (g:B → C) (h:C → D) #check comp #check comp f g #check f;g;h …

https://leanprover-community.github.io/install/windows.html MicrosoftリサーチはMicrosoft社の研究部門ではなく、 マイクロソフトリサーチ ： 完全に独立した研究機関であり、そこで行われる研究内容については、たとえマイクロソフト本社の首脳陣であっ…

整理はされてないが列挙： ガッカリ・ウンザリするところがない。 しがらみの無さ 単一言語 構文の一貫性 → 予測可能性 将来性・期待感 歴史上初の汎用プログラミング言語へ Unicode文字キーワード → 可読性、視認性 薄いシンタックスシュガー（甘さ控えめ）…

CTRL+CLICK でリンクをたどって。 さくら（sakura）とGMO - (保存用) 檜山正幸のキマイラ飼育記 メモ編 GMO VPSの契約管理 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 再度ドメイン設定 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 GMO VPSの設定 - (保存…

http://watanabe-www.math.dis.titech.ac.jp/users/swatanab/Renshu_0.pdf このテキストでは、確率分布＝確率変数による前送り測度。確率変数は、確率空間（の台可測空間）からのRへの可測写像。

ヘミトレースは、対称モノイド圏に入るコンビネータ HX,A,Y: C(A, XY) → C(XA, Y) バニシング、タイトニング、スライディング、スーパーポージングはトレースと同じ。ヤンキングに対応する公理をクロッシングとする。 f;HX,XX,X(σX,X) = σA,X;HX,A,X(f) ヘミ…

http://www.paoloperrone.org/phdthesis.pdf に色々書いてある。面白い。 カントロビッチモナドの台関手がカントロビッチ／ワッサースタイン関手。 たちの良い距離空間Xに対して Wass(X) をワッサースタイン空間と呼ぶ。ワッサースタイン空間の台集合はラド…

条件や性質〈命題〉の定義と、モノの定義は違う。モノを定義するとは、存在させる〈make it exist〉こと。 生成 構成的生成 超越的生成 正当化：存在命題 → スコーレム関数〈選択関数 | セレクター〉 正当化：一意性命題 → 一意値 条件確認〈検証 | 正当化〉

次は同義語 多相型 総称型 型構成子 パラメータ付き型 インデックス付き型 型ファミリー 適切な言葉は型値関数、使うのは型ファミリーにする。型ファミリーとは、Xを集合として、F:X → |C| という写像。Cの対象を型と呼べば、型値関数。X⊆|C| のときが総称型…

ツリーデータ型のモナドのモナドを具体的に書き下すととなると、けっこう難しいようだ。何が障害かというと： 型がうまく定義できない。 空型と単位型 部分集合型、内包的記法 ベキ集合型 直積型 指数型 直和型 依存和型 依存積型 型カインド 処理がうまく書…

フレイド圏の一般化。複数の異なる（異なってもいい）ドクトリンの圏と、そのあいだの関手からなる構造。

わだち圏〈トラック圏 | track category〉は、今風に言えば (2, 1)-圏。 k ＞ 2 なk-射は自明 k ＞ 1 なk-射は可逆 ホム圏は亜群になるので、亜郡豊饒な圏。特別な例として： ホムセットが亜集合である圏＝ホムセットに同値関係が載っている圏 わだち圏をベ…

丸山先生の記事で、「アブラムスキー・クッカ対応」と書いてあったけど、「クッカ」に近いのか。それと、この対応はもっと昔の人の名前を使って「カリー・ハワード・ランベック対応」がより一般的だと思う。圏論と量子情報・計算を対応づけたのはアブラムス…

コンピューターサイエンスの学習は、職業エンジニアになることを阻害する https://zenn.dev/nakanishi/articles/d3d8ff5529832f2acf6c 言っていることは正しいし、こういう意見の人はけっこう多いけど、まとまった文章がないから助かる。記事を消してしまう…

＠2020-09-30 20：00--22:00 by Zoom vs にならなかった。 谷村先生の絵が力作。 パットナムの双子地球が批判されていた。 双子地球の“水”は、心的状態が一致しても外延が一致してない例らしい。 SF、ファンタジーとしては面白い気がするが、フィクションと…

*1 *1:https://www.monotaro.com/p/3578/6974/

印象 連想 憶測 共感 信頼

「用語ペアの関係性」の続き。 ⊆： 包含的 ⊆→ ： 規準的埋め込み可能 ⊥： 排他的 ∪： 総称 環、可換環、非可換環 用法 1： 環 ＝ 可換環 ⊆ 非可換環 用法 2： 可換環 ⊆ 非可換環 ＝環 用法 3： 可換環 ⊥ 非可換環、環 ＝ 可換環∪非可換環 数、単項式、多項式…

形容詞を 原子＝基本＝単純 として使おうと思っても： 原子論理式 ＝ 基本論理式 ＝ 単純論理式 ： OK 原子定理 ＝ 基本定理 ＝ 単純定理 ： 定理という名詞の意味から、基本定理、単純定理は別な連想が働く。 同義語扱いを増やすと、区別したいときに困る。…

基底変換、なにそれ？ - 檜山正幸のキマイラ飼育記 (はてなBlog) 「空間」と呼ぶが、空間ではないし（位相はないし）、群作用の特殊例。 随伴系はなぜ難しいか - 檜山正幸のキマイラ飼育記 (はてなBlog) 「ペア」と呼ぶがペアだけでは意味がない。

まだまだ改善の余地がある。コンパクト論理に限定するとして、 論理式＝生成対象の集合 F から作った自由コンパクト圏 原子証明＝生成射＝シーケントの集合 S から作った自由コンパクト圏 コンパクト圏〈コンパクト閉圏〉は、射の同値書き換え〈equivalent r…

形式的に定義しない言葉 証明 → 証拠{図 | 式}またはリーズニング{図 | 式} 公理 → 原子定理 命題 → 論理式、定理 推論、推論規則 → 原子証拠{図 | 式}、原子リーズニング{図 | 式} 形式的に定義する言葉 項、原子項 論理式、原子論理式 文脈 シーケント 証…