Hatena Blog Tags
はてなブログ トップ
カリー=ハワード同型
このタグでブログを書く
言葉の解説
ネットで話題
関連ブログ

カリー=ハワード同型

このタグの解説についてこの解説文は、すでに終了したサービス「はてなキーワード」内で有志のユーザーが作成・編集した内容に基づいています。その正確性や網羅性をはてなが保証するものではありません。問題のある記述を発見した場合には、お問い合わせフォームよりご連絡ください。
曇りなき眼で見定めブログ•2年前

ジラール先生の"Proofs and Types"の3,4章を(ちょっと真剣に)読む（カリー=ハワード同型、正規化定理）

↓これの続きでっせ。 cut-elimination.hatenablog.com 3章は型とは何かという哲学的な考察を含んでいる。4章は正規化定理を解説したテクニカルな内容である。 Chapter 3 カリー=ハワード同型 命題を型と対応させる。型付項のシステムにおいても sense と denotation の二項対立が現れる。denotation はプログラムの denotational semantics（表示的意味論）の背景にある。もちろん。それは denotation の等式を与える静的なものである。対して sense の方は操作的意味論をもたらす。こちらは書換えを与える動的なもの…

#ジラール#カリー=ハワード同型#正規化定理

ネットで話題

もっと見る
39ブックマークHaskell/カリー=ハワード同型 - Wikibooksカリー=ハワード同型(Curry-Howard isomorphism)は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。 これよりカリー=ハワード同型は単に C-H と表記する。C-H が示しているのは、定理の本質を反映するような型を構築し、それからその型を持つ値を見つけさえすれば、どんな...ja.wikibooks.org
34ブックマークカリー＝ハワード同型対応 - Wikipediaja.wikipedia.org
12ブックマークカリー・ハワード同型対応入門takuro.onishi@gmail.com II 2009 6 4 11 • Figure: H.B.Curry (1900-82) Figure: W.A.Howard (1926-) • 1934 1958 • 1968 • • • • • • • • • • • • • • • • • • • • 3.6 (an)n (an)n (an)n 3.5.1 (an)n (an)n 3.5.2 (an)n (an)n (an)n • ( 1980, pp. 26-27) • ABCD ABCD ABCD 4 A, B, C, D ABCD ABCD ABCD n 4 n 2 n 4 ...ocw.kyoto-u.ac.jp
9ブックマークカリー=ハワード同型対応にびっくり - うつし世はゆめ / 夜のゆめもゆめ知の教科書 論理の哲学 (講談社選書メチエ) 飯田隆(編) 講談社、2005 ↑の本のいくつかの章をコピーして読んでいた。 照井一成「計算と論理」は、カリー=ハワード同型対応の解説。ほうほうと思って読んでたらこれがびっくり。 カリー=ハワード同型対応って、「論理学の証明と関数型言語のプログラムが一対一対応する」と...www.at-akada.org

関連ブログ

takashina tokiosa•17日前

グーゴロジストのためのBuchholz's ψの周辺知識

（執筆中） Buchholz’s ψの周辺知識を備忘録的にまとめておく。 筆者は数学を専攻していないので、鵜呑みにはしないでほしい。 1.巨大数論的文脈 巨大数論においては、Buchholz's ψ・Buchlolz's hydra・ペア数列・段階配列表記は同じくらいに急増大する関数を与えることが知られている。 ペア数列は2行のバシク行列であって、非常に重要な位置を占めている。 段階配列表記は横ネスト段階配列表記へとつながるmrna(伝)氏による一連の研究の足掛かりとなっている。 また、EBO(拡張Buchholz Ordinal)やψ系表記の元になっているともいえる。 よって、多くのグーゴロ…

soukouki’s diary•7ヶ月前

セキュリティキャンプ2024 Cコンパイラゼミ 応募課題晒し

セキュリティキャンプ2024のCコンパイラゼミについて、選考に通過したので応募課題を公開したいと思います。 セキュリティキャンプに応募するのは今回が2回目です。前回はエントリーだけして、応募課題を前にして諦めてしまった記憶があります。今年の春になり、去年参加した友人の勧めで今年も応募しました。今は浪人・留年のない学部4年生なので、今年が応募できる最後のチャンスということになります。今年受かって本当に良かったです。 応募したのは開発コースの「Rust プログラム検証ゼミ」と「Cコンパイラゼミ」です。一応第3希望として他のゼミも応募したのですが、第2希望までの応募課題で力尽きてしまったので、この2…

zakkyの雑記•8ヶ月前

『論理と計算のしくみ』を読んだ

計算機科学の入門書である『論理と計算のしくみ』を読んだ タイトルの通りで、GWの前半を使って『論理と計算のしくみ』という本を読んだ。 https://www.amazon.co.jp/dp/4007305803/ 実はこの本自体は、エンジニアとして仕事をし始めた5年前のタイミングで購入していた。 いわゆる積読状態だったのだが、流石に5年も寝かせたままなのもな…と思い一念発起して読んだ。 感想はと言うと、読んで良かったな〜としみじみする本だった。 それだけだと全然伝わらないと思うので、箇条書きで良かった点を書くと、 基礎的な集合論や命題論理、様相論理をコンパクトに解説してくれている 集合論と論理…

純ブログ•10ヶ月前

YAPC::Hiroshima 2024に行ってきた

YAPC::Hiroshima 2024の前夜祭と本編に行ってきました。 別のことにかまけていたらブログを書くのが遅くなってしまいました...。 YAPCに現地参加したのはコロナ禍前のYAPC::Tokyo 2019以来2回目です。 What I Like YAPC::Hiroshima 2024のテーマが「What You Like」ということで、 私のお好みは... What I like... Perl TypeScript 型 です。 Perl 業務でいつもお世話になっている言語です。 なんとなく「手作り感」があるのが好きなところです。 TypeScript 昨年静的サイトを構築するた…