Hatena Blog Tags
はてなブログ トップ
シーケント計算
このタグでブログを書く
言葉の解説
ネットで話題
関連ブログ

シーケント計算

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

ジラール先生の"Proofs and Types"の5,6章を(ちょっと真剣に)読む（シーケント計算、強正規化定理）

↓これの続きでこざる。 cut-elimination.hatenablog.com シーケント計算 シーケント計算は自然演繹ほど計算との対応が明確ではないとのことだった。しかしPROLOGの基礎になっていたり自動定理証明に使われるタブローの一般化でもあるという。これは知らなんだ。私はPROLOGの仕組みを知らないので調べねばね。タブローがシーケント計算の一部だというのは分りそうで分らない。。。 続いてシーケント計算が定義される。構造規則が思いの外重要であるとある。確かに構造規則が重要だからこそ構造規則を制限した線形論理が生れた訳だ。 前回までであまりピンときていなかった対称性が分ってきた。シ…

#ジラール#シーケント計算#強正規化定理

関連ブログ

檜山正幸のキマイラ飼育記 (はてなBlog)•1ヶ月前

複圏〈オペラッド〉とプレ準同型射の圏

「論理や型理論の圏論的意味論 // 導出システムの圏と圏の圏」において、導出システム達を対象とする圏に触れました。しかし、導出システムのあいだの準同型射（それが圏の射となる）を素朴に考えていては、どうもうまくないようです。導出システムは、複圏〈オペラッド〉と密接に関係があります。導出システムの代わりに、複圏が対象であるような圏をまずは考えてみます。複圏のあいだの射は、通常の準同型射ではなくて、もっとゆるい概念であるプレ準同型射とします。複圏〈オペラッド〉を対象として、複圏のあいだのプレ準同型射を射とする圏が、導出システムの記述と分析にふさわしい気がします。$` \newcommand{\mrm…

檜山正幸のキマイラ飼育記 (はてなBlog)•2ヶ月前

型理論の演繹定理

過去記事「矢印記号の使用法と読み方 2024」において、様々な矢印記号の意味・運用について述べました。構文論で使う矢印記号に関して、別な読み方・名前を追加して一覧表を再掲します。 矢印記号 読み方 別な読み方・名前 $`\Rightarrow`$ 含意〈implies〉 関数型〈function type〉 $`\vdash`$ 伴意〈entails〉 判断ストローク〈judgement stroke〉 $`\rightrightarrows`$ 推論〈infers〉 (特になし) $`\Vdash`$ 正当〈correct〉 整形式性〈well-formedness〉 $`\Vvdash`$…

(新) 檜山正幸のキマイラ飼育記 メモ編•2ヶ月前

型理論-論理の用語対応表 n回目

型理論 論理 集合圏 Set 論理圏 Logic 型のポイントインスタンス 命題の証拠 引数リスト 前提〈仮定 | 仮説〉リスト 関数 定理 戻り値型 結論命題 関数の計算 定理の証明 関数のプロファイル 定理のステートメント トップダウン関数定義 バックワード・リーズニング ボトムアップ関数定義 フォワード・リーズニング ラムダ計算 自然演繹 コンビネータ計算 シーケント計算 関数コンビネータ リーズニング規則 関数の定義行為 定理の証明行為 プログラミング 証明行為 プログラムコード 証明コード〈項 | スコア | 譜〉 関数の本体コード 定理の本体コード〈項 | スコア | 譜〉 計算項…

檜山正幸のキマイラ飼育記 (はてなBlog)•2ヶ月前

カリー／ハワード／ランベック対応のための“呼び名”と“書き方”

ここ最近の本ブログのテーマは「カリー／ハワード／ランベック対応」です。最近の記事がすべてカリー／ハワード／ランベック対応に関係するわけではありませんが、9月の記事「関数の構成法 (カリー／ハワード／ランベック対応も少し)」あたりから、カリー／ハワード／ランベック対応についてまた考える機会が増えました。以前からの悩みのタネなんですが、「カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏」で書いたこと： この綺麗な対応がなかなか伝わらないようです。対応が見えにくくなっている大きな原因は、構造が綺麗に対応していても、言葉や記号は対応してないことです。論理／型理論／圏論の三者において、まっ…

檜山正幸のキマイラ飼育記 (はてなBlog)•3ヶ月前

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

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

檜山正幸のキマイラ飼育記 (はてなBlog)•3ヶ月前

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

昨日の記事「エンテイルメント記号とシーケント」において、従来のシーケントの書き方は変更したほうがいいと提案しました。この機会に、シーケントに対する長年の不満とその対策を記しておきます。$` \newcommand{\Imp}{\Rightarrow } \newcommand{\Ent}{ \sqsubseteq } `$内容： シーケントの書き方 コンパクトシーケント 右単元シーケントと左単元シーケント 右片側シーケントと左片側シーケント 名前付きと名前無し シーケントと判断 導出可能性 おわりに シーケントの書き方昨日の記事「エンテイルメント記号とシーケント」の要点は、シーケントを次のよう…

檜山正幸のキマイラ飼育記 (はてなBlog)•3ヶ月前

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

「記号のグリフと使用場面・使用意図： 型理論、圏論、集合論、論理など」において、矢印記号 '$`\to`$' やターンスタイル記号 '$`\vdash`$' のオーバーロードとコンフリクトが長年の悩みの種であることを述べました。上記過去記事で次のように書きました。 エンテイルメント記号は、圏論のプロファイル矢印とコンフリクトしますが、これはしょうがないです。昔は、エンテイルメント記号に '$`\vdash`$' を使うことがありましたが、型理論との記号の奪い合いの抗争に疲れたので、今は使いません（'$`\vdash`$' は型理論に譲った）。述語と部分集合の一対一対応を強調するときは、エンテイ…

檜山正幸のキマイラ飼育記 (はてなBlog)•8ヶ月前

方向・向きの話： 高次圏を語るために

この記事の目的は、「上下」「左右」「前後」などの言葉の意味をハッキリさせることです。動機は、高次元の圏 -- あるいは圏類似代数系〈category-like algebraic {structure | system}〉について、行き違い／誤認がないように語りたいからです。最近の応用圏論〈ACT | Applied Category Theory〉では、1次元の圏だけではなくて、2-圏、二重圏、3-圏、三重圏などが出現します。それらに関わる概念の描画には、2次元または3次元のストリング図やペースティング図が使われます。この状況で、「上下」「左右」「前後」などの意味が曖昧だと、コミュニケーショ…

檜山正幸のキマイラ飼育記 (はてなBlog)•10ヶ月前

命題と判断

久々に論理の話をします。論理とはいっても、形式化された論理〈formal logic〉の話ではなくて、“ちゃんと考えるための技法”といった意味の論理です。「命題と判断は区別しましょう」が僕がこの記事で言いたいことです。$`\newcommand{\Holds}{ \mathrel{|\!-!} } \newcommand{\Ques}{ \mathrel{|\!-?} } \newcommand{\HHolds}{ \mathrel{||\!-!} } \newcommand{\HHHolds}{ \mathrel{|||\!-!} } \newcommand{\NotHold}{ \math…