コンビネータ
【combinator】自由変数を含まないλ式のこと．
計算論を始めとしてλ式，λ計算を扱う理論において重要視されている．λ計算において対象をコンビネータのみに制限したものをコンビネータ論理と呼ぶこともある．
このタグの解説について
この解説文は、すでに終了したサービス「はてなキーワード」内で有志のユーザーが作成・編集した内容に基づいています。その正確性や網羅性をはてなが保証するものではありません。問題のある記述を発見した場合には、お問い合わせフォームよりご連絡ください。関連ブログ
Scheme 手習い（10）~ eval と apply ~
第10章：このすべての値は何だ Scheme 手習い第 10 章。 いわゆる eval を実装する。この本では value という関数名になっているけど。 準備 リストを操作するための便利関数を事前に定義しておく。 (define (build a b) (cons a (cons b '()))) (define (first x) (car x)) (define (second x) (car (cdr x))) (define (third x) (car (cdr (cdr x)))) エントリーとテーブル（環境） new-entry (define new-entry build)…
ネットで話題
もっと見る
yj.chibicode.com
wired.jp
nowokay.hatenablog.com
naze.chibicode.com
amachang.hatenablog.com
r-west.hatenablog.com
wired.jp
logmi.jp
r-west.hatenablog.com関連ブログ
ベイズ確率論とデータベース理論の統合： カップル化可能圏
今年（2020年）の6月にマルコフ圏というものを知りました。 マルコフ圏 A First Look -- 圏論的確率論の最良の定式化 マルコフ圏の直接的応用は圏論的確率論（「圏論的確率論におけるCタイプとAタイプ」参照）ですが、他の分野への応用もありそうです。「マルコフ圏の一族」より引用： マルコフ圏が応用できそうな分野には、データベース理論、形式言語理論、オートマトン理論、プログラム意味論などがあります。これらはたまたま僕が少し知っている分野で、他にも物理や工学などに応用可能ではないかと思います。 当初から、マルコフ圏はデータベース理論とは親和性が高そうだと感じていました。一方、ここ一週間く…
Scheme 手習い（９）~ Y コンビネータ~
第9章：…… もう一度、もう一度、もう一度、……（続き） 第9章の最後は Y コンビネータについて。 リストの要素数を数える length を題材にして Y コンビネータを学ぶ。 length リストの要素数を数えるなんの変哲もない関数 length を定義する。 (define (length l) (cond [(null? l) 0] [else (add1 (length (cdr l)))])) length を define を使わずに定義できるだろうか？ define がなければ、関数名を定義できないので定義内で自身を参照できない。 これでは再帰ができないので length は定…
Scheme 手習い（８）
第9章：…… もう一度、もう一度、もう一度、…… keep-looking (define (pick to lat) (cond [(= to 0) (car lat)] [else (pick (- to 1) (cdr lat))])) (define (keep-looking a to lat) (cond [(number? to) (keep-looking a (pick to lat) lat)] [else (eq? a to)])) 引数のインデックスの要素が数字かシンボルかを判定する。 数字だった場合にはさらにその数字をインデックスとして要素を取得して同じ事を繰り返す。…
随伴系の反転置写像とモナドのクライスリ拡張
用語と記号のオーバーロード〈多義的使用〉はホントに悩みのタネです。混乱と誤解を避けるためにオーバーロードはやめようと思うことは多いのですが、あまり律儀にオーバーロード解決すると用語と記号のインフレーション〈急激な増加〉を引き起こして現実的ではありません。習慣や癖、あるいは不注意からオーバーロードを使ってしまうことがあります。それでトラブルにならなければいいのですが、混乱と誤解の原因を作ってしまったときは「あー、やっちまった」と後悔します。内容： 随伴系の反転置写像 モナドのクライスリ拡張 クライスリ拡張と自由拡張 随伴系の反転置写像随伴関手ペア〈adjoint pair of functors…
マルコフ核の随伴公式とフビニの定理
昨日の「拡張スタイルのジリィモナド」にて： 随伴公式は積分のフビニの定理です。ただし、マルコフ核が絡むと、単純なフビニの定理と少し違った形になります。単純なテンソル積測度ではなくて、依存テンソル積とでも呼ぶべき構成が必要です。が、この話題は別な機会にします。 こいうことを書いてよくあるパターンは、「別な機会」が2年後になったり、永久に書かなかったり（たち消え）。間をおかずに書いてしまうのが吉です。マルコフ核の随伴公式は、フビニの定理に帰着されます。そのフビニの定理も、ある種の随伴公式だということを説明します。が、大ざっぱな説明です。昨日の記事は読んでなくてもかまいませんが、次の記事に目を通して…
絵算で見る、拡張スタイルのモナドとモノイド・スタイルのモナド
「Haskellの二重コロン「::」とバインド記号「>>=」の説明」で、拡張スタイルのモナドとモノイド・スタイルのモナドの話題が出ました。この話題はだいぶ昔に書いたことがありますが、絵算の応用として「拡張スタイル ←→ モノイド・スタイル」の相互変換をしてみます。内容： 絵算の技法 モノイド・スタイルのモナドの定義 拡張スタイルのモナドの定義 モノイド・スタイルから拡張スタイルへ 拡張スタイルからモノイド・スタイルへ 素材の準備 拡張スタイルからモノイド・スタイルへ 法則の証明 おわりに 絵算の技法モナドの二種類の定義を行ったり来たりする、つまり「拡張スタイルのモナド ←→ モノイド・スタイル…
論理の用語法整理の試み
「原子」「複合」 を使う。次の表の欄に入る語は正式なテクニカルタームとして定義する。 原子 (複合) 構成規則 項 論理式 証明 リーズニング リーズニングが一番ゴタゴタで、 証明{図}?の構成規則の概念とかぶる。 コンビネータ由来のリーズニングと、2-射由来のリーズニングがある。 フォワードリーズニングとバックワードリーズニングがある。 テクニカルタームとしての定理は3種類。 論理式定理： 論理式に名前を付けて、証明部として証明を付けたもの。 証明定理： 証明に名前とプロフィールを付けて、証明部としてリーズニングを付けたもの。 論理式定理のとき： ステートメントとは論理式そのもの。 証明部は…
ICFPC 2020 galaxy.txt を読む (その 1: decompile)
その 0 で ICFPC 2020 をざっと復習しました。では実際に galaxy.txt を見てみます。 galaxy.txt 開いてみると、以下のようになっています :1029 = ap ap cons 7 ap ap cons 123229502148636 nil :1030 = ap ap cons 2 ap ap cons 7 nil ... :1107 = ap ap c ap c ap ap b :1183 ap ap c ap ap c :1221 0 ap ap cons 2 ap ap cons 2 ap ap cons 0 ap ap cons 0 ap ap cons…
ICFPC 2020 galaxy.txt を読む (その 0: ICFPC 2020 振り返り)
一月ほど前の 2020/07/17-20 に ICFPC 2020 がありました。今年はここ最近多い対ゲーム的なものに加えて、ちょっと凝ったストーリーとちょっとした interpreter (Garaxy Pad) を作る必要がありました。この Garaxy Pad に、開始数時間後に与えられる galaxy.txt を実行させると、対戦ゲームのチュートリアル的なことができたわけですが、多分コンテスト期間中に galaxy.txt を読もうとした人はほとんどいないと踏んで、解説を書いてみました。 ストーリー/仕様振り返り まず galaxy.txt を読むのに必要な範囲でストーリーと Gala…
色々な対応関係
暫定案、後で修正。日本語だと複数形がないので、複数形の代わりに「ナントカセット」とする。 セオリー論 プログラミング 論理 ストリング図 指標 インターフェイス 推論規則セット スパイダーセット〈アイコンパレット〉 ソート 型 命題 ワイヤー（のラベル） オペレーション サブルーチン 定理 名前付きストリング図 基本オペレーション 組み込みサブルーチン 公理 スパイダー オペレーション宣言 サブルーチンプロトタイプ 定理宣言 - オペレーションボディ サブルーチンボディ 定理の証明 名前付きストリング図のストリング図 リファクタリング 証明の書き換え ストリング図の書き換え 構文モナド プログ…
マルコフ圏から付点構成／合同商構成でダガー対称モノイド圏を作る
過去の記事「マルコフ圏におけるベイズの反転定理」の最後で次のように言いました。 「ベイズ反転は、ほんとの逆射ではないから inversion と呼ぶのは不適切」という意見はもっともですが、適当なセッティングのもとでは、ベイズ反転を逆射と考えることが出来る気がします。今のところ確証はないですが、状況証拠は幾つかあります。「ほんとの逆射」まではいかないかも知れませんが、逆射扱いしていい状況がありそう。もし、ベイズ反転を逆射扱いしていいなら、計算はだいぶ気楽になります。ちょっと考えてみますわ。 この件、考えてみました。けど、フリッツ〈Tobias Fritz〉のテキストに必要なことはだいたい書いてあ…
確率的圏における期待値と雑音
確率的圏〈stochastic category | 確率圏〉の暫定的定義については「確率的圏、存在命題とスコーレム・コンビネータ // 確率的圏」で述べました。確率的圏は、事実上ジリィモナドのクライスリ圏です。こう定義してみても、期待値の概念は現れません。期待値を計算することは多いので、圏論的確率論で期待値が扱えないのは困ります。とりあえず、特定の目的を想定して、そこで使えそうな期待値概念を定義しましょう。特定の目的とは、「雑音が乗る／真の値を推測する」という言葉にハッキリした意味を与えることです。[追記]この記事は、使っている記法の関係で読みにくいかも知れません。読みにくさの原因や対処につ…
2020年の目標 - 7月まとめ
引きこもり生活5ヶ月目。 osak.hatenablog.jp どうせフルリモートだし、チームメンバーもいつもより出力速度が遅いので、もっと適当に仕事してもいいんじゃないかと思って勤務時間を勝手にシフトし始めた。だいたい夜のほうが調子がよいので、朝から昼のミーティングに出てコードレビューとかしたら昼寝して、夜にちゃんとコード書いたり面倒な設計とか考えたりする感じで……。あと夜がんばって仕事したら翌日は遅く起きるとか。そもそも眠い時に頑張って起きててもロクな出力は出てこないので寝るのが正しいと思う。 ゲーム。ICFPCやった。アトリエシリーズに敬意を表してチーム名はAtelier Manarim…
確率的圏、存在命題とスコーレム・コンビネータ
以前に書いた記事「圏論的確率論におけるCタイプとAタイプ」と、昨日書いた記事「マルコフ圏におけるベイズの反転定理」に対する補足を書きます。内容： 確率的圏 確率的圏の事例 存在命題 スコーレム・コンビネータ 確率的圏確率的圏〈stochastic category〉とは何か？ 広く合意された定義はありません。が、曖昧なまま言葉を使うのはコミュニケーションに差し障りがあるので、暫定的あるいはローカルな定義をしておきます。Measを、すべての可測空間と可測写像からなる圏として、Meas上のジリィモナドを Giry = (Giry, μ, η) （記号の乱用）とします。すると、圏Stocは、ジリィモ…
