Closed dannypsnl closed 7 months ago
喔!另外一定要談到這就是為什麼 inductive/coindcutive 是 initial algebra
啊這個應該可以寫成 algebra of an endofunctor $F$ is a morphism $F x \to x$
想請教,關於 initial object 跟 terminal object 在這裡起什麼作用,為什麼會需要這兩個東西
因為對固定的 F 來說,它全部的代數構成的範疇的 initial 跟自己的原始物件同構,也就是令 $F\ i$ 為 $F(C)$-initial 則 $F\ i \cong i$,也就是其代數 $F\ i \to i$ 是一個 $C$-isomorphism
我可以翻譯這篇,可能會順便從中提出一些我不太了解的部份當作是一種 Q&A
這圖要怎麼畫出來
quiver: https://q.uiver.app/
但在 forester 裡面要寫成 \tex{\begin{tikzcd}\end{tikzcd}}
不知為啥會有 error,在之前的語法裡完全沒問題
Texlive 可能要檢查一下吧?我用 Mac 試試看
我這邊沒問題,所以應該是 latex 的毛,你可以複製有問題的指令(有印出)然後到 build 目錄裡面測試一下
我把 texlive 重裝成 2023 版本還是有會有錯,但目前追蹤到的是執行 pdflatex 這個指令時出問題,不過不知道從何修起 😢
我覺得可以嘗試把 amsthm 直接引用,然後把上面的 ifpdf 條件式去掉之類的,去看在哪裡出錯
另外就是你用哪個 texlive,相關資訊應該可以查一下
我有嘗試把 tikzcd 的內容修改 這樣可以動
\begin{tikzcd}
a
\end{tikzcd}
這樣會噴錯
\begin{tikzcd}
\bullet
\end{tikzcd}
太神奇了,可能 \bullet
是什麼套件提供的?
我懷疑我少裝什麼導致無法解析
最新進展,\bullet
, \cdot
兩個都沒辦法用
可能是我字體問題,但我實在沒心力 debug
不過還好目前的圖都用不到 \bullet
, \cdot
這是關於 F-algebra 一些提問
一開始所寫的簽名我們該怎麼解讀它
\begin{cases}
1:1\to m \\
\bullet: m \times m \to m
\end{cases}
我們怎麼從上方得出這個態射的 $1+m \times m \to m$
可能需要一些實際案例,讓讀者能夠想像
取簽名裡面所有 ... -> m
的 ...
群環體對數學背景的人來說應該很具體,要程式的案例的話 inductive types 就是了
當然 inductive types 是這些推理的結果,你需要什麼樣的案例?
這邊倒是還好,主要是 Catamorphism 那邊的不動點需要一點案例
或者我們可以後續用一個 Functor 實作來呼應這邊的內容
那你應該可以用 ListAlg 試試看,後面應該是沒必要,因為 catamorphism 不怎麼實用,主要還是一種數學上的關聯
案例的話,在 PR 修完之後可以看這篇《Clowns to the Left of me, Jokers to the Right》
這篇是文章嘛,還是書
論文
另一篇有用的論文是
《Containers: Constructingstrictly positive types》 M. Abbott et al. / Theoretical Computer Science 342 (2005) 3 – 27
這個是上面 Clown Joker 講到的 container functors 的細節
Clowns to the Left of me, Jokers to the Right 這篇要去哪裡找
翻譯這篇 https://dannypsnl.me/math-001K.xml 到 repo