このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

2024-09-01から1ヶ月間の記事一覧

インターフェイスとしての指標、設計者と利用者と実装者

指標〈signature〉と呼ばれる構文的形式は、数学ならば公理系の記述に使われます。例えば、群の公理系とか可換環の公理系とかを指標で書けます。ソフトウェア/プログラミング分野の言葉で言うなら、指標はインターフェイスです。インターフェイスには、それ…

関数の構成法 (カリー/ハワード/ランベック対応も少し)

与えられた関数達を素材にして新しい関数を作り出すこと -- これは基本中の基本ですね。でも、整理されてないかも知れません。整理しましょう。$` \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1}} %\newcommand{\msf}[1]{\mathsf{#1…

シーケントに関する不満と対策

昨日の記事「エンテイルメント記号とシーケント」において、従来のシーケントの書き方は変更したほうがいいと提案しました。この機会に、シーケントに対する長年の不満とその対策を記しておきます。$` \newcommand{\Imp}{\Rightarrow } \newcommand{\Ent}{ \…

エンテイルメント記号とシーケント

「記号のグリフと使用場面・使用意図: 型理論、圏論、集合論、論理など」において、矢印記号 '$`\to`$' やターンスタイル記号 '$`\vdash`$' のオーバーロードとコンフリクトが長年の悩みの種であることを述べました。上記過去記事で次のように書きました。 …

プログラミング言語としての Powershell の印象

Windows OS において、バックアップスクリプトを書こうとしたのですが、cmd.exe のバッチファイル〈.batファイル〉で書くのは辛いので Powershell のスクリプト〈.ps1ファイル〉として書くことにしました。Powershell は、シェル(OSのコマンドラインUI)と…

追記: ターンスタイルのオーバーロードの弊害

「型理論のコロン、ターンスタイル、カンマ」への追記ですが別記事にします。ターンスタイルをオーバーロードすることの弊害は、(ターンスタイルに限らないけど)ターンスタイルが表す複数の意味がゴッチャになりがちなことです。もちろん、区別できる人は…

型理論のコロン、ターンスタイル、カンマ

昨日の記事「記号のグリフと使用場面・使用意図: 型理論、圏論、集合論、論理など」より: なんでそこまでコロンとターンスタイルにこだわるのか? 僕にはちょっと意味不明です。...[snip]...僕の個人的感想としては、型理論独自の記法をやめて、圏論と集合…

記号のグリフと使用場面・使用意図: 型理論、圏論、集合論、論理など

あっ、そうか! と気が付きました。型理論、圏論、集合論、論理などを一緒にやるときに、同義語・多義語に悩まされるのですが、記号に関しても同義記号・多義記号のカオス状態にストレスがたまります。例えば、矢印記号に関しては次の過去記事に書いています…

型理論のインスタンスとは

型理論の「インスタンス」の意味がハッキリしないのですが、次の3種にわければだいたい説明が付きそうです。 一般インスタンス ポインティングインスタンス セクションインスタンス 圏論的な解釈をします。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand…

実用になる型理論の記法

型理論では、「代入〈substitution〉」という言葉を幾つかの意味で使います。この記事では複数の意味を切り分けて別な呼び名を与えることにします。ある人々にとっては、いちいち呼び分けることは鬱陶しくてバカバカしいことに思えるでしょう。しかし、誰も…

GAT〈ガット〉の構文: スターリングの論文から

過去記事「GAT〈ガット〉」で、次の論文に言及しました。 [Ste19-] Title: Algebraic Type Theory and Universe Hierarchies Author: Jonathan Sterling Submitted: 23 Feb 2019 Pages: 25p URL: https://arxiv.org/abs/1902.08848 6月にチラ見しただけなの…

ペアの形式的な定義

公理的集合論やグロタンディーク宇宙の公理系では、順序を持たないペアが作れることは保証しています。が、順序を持つペアは頑張って作るのが普通です。作り方は一通りではありません。典型的な順序ペアの作り方を見ておきましょう。$`\newcommand{\mrm}[1]{…

置換公理に出てくる「関数」とは

公理的集合論の置換公理を「関数の像は集合である」と説明したり理解したりする人がいます。まー、そうなんですけど、ここに出てくる「関数」を普通の意味で理解すると、まったくのトンチンカンなことになります。置換公理に出てくる「関数」は、普通の関数…

カートメル/ヴォエヴォドスキー/パルムグレンの型理論

型理論/型システムは何十種類、いや何百種類もあるのですが、そのなかで、「今のイチ推しは何ですか?」と聞かれれば、カートメル/ヴォエヴォドスキー/パルムグレンの型理論を挙げます。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{\text{ i…

「命題」の曖昧性から前層意味論へ

「命題」という言葉は極めて曖昧な言葉です。曖昧だから色々な意味で使えて便利ということでもあります。使う場面・文脈により次のような意味があります。 真偽値 述語 論理式 定理 (国語辞書的意味で)課題、使命、目標など この曖昧性については、「Propo…

デジタル語彙目録:: 名前の構造 再考

デジタル語彙目録における“管理された名前”〈managed name〉は、何らかの対象物を一意非曖昧に名付けるために使う人工的な名前です。通常のコミュニケーション内で管理された名前を直接使うことは意図してません。通常のコミュニケーション内で使う用語〈テ…