Agda による圏論入門
Menu Menu Agda で証明しながら圏論を学ぶという予定です。あまり入門ではないかも。 Higher-Order Categorical Logic の 0章に相等する内容です。 BitBucket category-exercise-in-agda source code Agda の入門の要約 Agda の入門 Agda の集合の Level Agda の record Agda のReasoning Caategory module と圏の入門 自然変換 IdentityFunctor と Hom Reasoning Monad の結合則 Sets と Monoid を使った Monad の例 Kleisli 圏の構成 ここまでが Monad を理解するための部分。以下は、Adjoint 関連です。 Adjoint から Monad を導く Kleisli 圏による Mona
コーディングに対する考え方を変える6つのプログラミングパラダイム | POSTD
私は時折、コーディングに対する考え方を変えさせられるような、従来と非常に異なるプログラミング言語に出会います。本記事では、その中でも特に気に入っている発見をいくつかご紹介したいと思います。 これは、先賢による「関数型プログラミングは世界を変える！」的な投稿ではありません。本記事で挙げるのは、もっと「知る人ぞ知る」的なリストです。多くの読者の方にとって、以下の言語やパラダイムは聞いたことのないものが大半だと思いますので、私が経験したように、これらの新しい概念を学ぶ楽しさを感じていただければ幸いです。 注：私は以下の言語の多くに関して最低限の経験しかありません。その発想に引き込まれたのであって、専門的知識は持ち合わせていないため、訂正すべき点や誤りがあればどうぞご指摘ください。また、本記事で取り上げていない新しいパラダイムや概念に出会った方は、ぜひお知らせください。 最新情報：本記事が r/p
Agda 入門
証明支援系の言語である Agda の入門を目的としています 具体的には Agda による証明の方法を知る 実際に自然数に対する演算の証明を追う ことをしていきます 証明支援系と呼ばれる分野の言語です 他には Coq などがあります Haskell で実装されています 型が非常に強力で表現力が高いです 命題や仕様を表す論理式を型として定義することができます 例えば 1 + 1 = 2 とか Agda における証明は 証明したい命題 == 関数の型 命題の証明 == 関数の定義 として定義します 関数と命題の対応を Curry-Howard Isomorphism と言います どうしてプログラムで証明できるかというと (命題 と 定義) は (仕様 と 実装) のように対応します int chars_to_int(char * chars) つまり char * から int は作れる、という
CoqのtacticやコマンドとAgda上操作の対応 - ぼくのぬまち 出張版
この記事は Theorem Prover Advent Calendar 2013 1日目の記事です． 注意事項がひとつあります．本記事にはAgdaコードを含めようとしていますが，記事内でちゃんと書けてない文字があるかもしれません．だが私は悪くねぇ！ ﾊヽ／::::ヽ.ヘ===ｧ {::{/≧=＝=≦V:/ >:´:::::::::::::::::::::::::｀ヽ、 γ:::::::::::::::::::::::::::::::::::::::::ヽ _／/::::::::::::::::::::::::::::::::::::::::::::::ﾊ 私知ってるよ . | ll ! :::::::l::::::/|ハ::::::::∧::::i :::::::i みんなCoqの記事ばっか書くってこと ､ヾ|:::::::::|:::/｀ト-:::::/ _,X:j
未来言語Agda - 数学猫の生活と意見
最近Agdaを触る機会があったのだが、Agdaこそ未来のプログラミング言語ではないかという気がしてきた。ここでは行列の転置をする関数を定義することで、Agdaでのプログラミングがどんなものか紹介したい。その前に一言:Agdaは定理証明系として紹介されることが多い。これはAgdaにとって不幸なことだ。確かにAgdaの型システムは強力なので、例のカリーハワード同型により、型を命題、プログラムを証明とみなすことができる。ただし、私の印象ではAgda上は数学の証明をしやすいようにはそんなにはできていない。Agdaで証明するには、ある型をもつ定数なり関数を定義することになるわけだが、定義した関数がその型を持っているかことを型チェッカに説得するために、型チェッカの詳しい挙動について理解していなければならない。むしろ、Agdaは依存型をもつプログラミング言語と思った方がよいと思う。依存型とはなにかは例を
Agda 入門＠ProofSummit 2011
The document summarizes features and updates in the Agda proof assistant. It discusses Agda tactics, the module system, compilation to Haskell and Epic, sized types, irrelevant declarations, termination checking, instance arguments, pattern matching lambdas, and plans for upcoming releases including JavaScript compilation and pattern matching lambdas. It also demonstrates some Agda code examples.R
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
