2022-04-24から1日間の記事一覧

型無し演算子指標とモデル

型無し演算子指標は untyped operator signature だが、untyped = single sorted 。また、演算子は代数的指標の演算〈operation〉。したがって、 op:(S, ..., S) → S と書ける。通常のプログラミング言語と同様に引数変数を使うと、 op: (a:S, ..., z:S) → …

リッチ述語、リッチバッグ、K集合

次の可換図式がある。$`\require{AMScd} \begin{CD} |{\bf FinSet}| @>{\mathrm{card}}>> {\bf N}\\ @AAA @AAA \\ |{\bf ThinSet}| @>{\mathrm{IsNonEmpty}}>> {\bf B} \end{CD}\\ \:\\ \text{commutative in }{\bf SET}`$やせた集合は空集合または単元集合…