Learn you An Agda And Achieve EnlightenmentRead It!
すっかり忘れてたけど、Agdaという名前の由来 - 旧・木下修司研究所
去年のProofsummitのときに、Agdaという言語はなぜそういう名前なのかという話を飲み会でしたら結構好評だったので、あらためて調べたことも含めて。 Agdaとは何かというと、これのことみたい。 実際、Agda the henでググってみると http://bit.ly/1aBKbbH という本が出てきて、明確に The name Agda comes from a Swedish song about Agda the Hen, a pun on the Coq rooster. と書いてある。(le )Coqはフランス語で雄鶏。で、Agdaはフランス語じゃないけど、スウェーデンの歌に出てくる雌鶏の名前ですよと。 で、さらによくできている話が、Coqを作った人のひとりThierry Coquand*1の奥さんCatarina Coquand（この人ですね）がAgda1の開発メンバの
Classical set theory in Agda - Just $ A sandbox
Agda歴2週間くらいのザコです。 Agdaで圏論のライブラリを作って、流れで位相空間の定義をしようと思ったらそもそも集合を普通に扱えるライブラリがどこにもない。 標準ライブラリにRelation.Unaryとかいうのもあるけど、これは表面的には上手く行っているように見えるだけであんまり使い物にならない。 具体的に言うと和集合の公理がないので(binary cupとindexed bigcupはある)任意個のUnionがとれない。 他にも、そもそも∈の定義が函数適用なので X ∈ B と書いときにXとBでは型が違うのがすごくキモいとか。キモいというかこれのせいでZFの一部の公理は型があわなくて表現できなかったりもする。 そういうわけでまずは集合を使えるようにするというだけ。 コードは一番下に載っけました。 コードについて 二重否定除去 Relation.Nullary.Negation e
copatterns概要 - ぼくのぬまち 出張版
ghc-7.8でビルドできるAgdaマダカナーとか思いつつ，Agda-2.3.4のリリースノート(まだリリースされてないけど)を眺めてたら，実験的機能としてcopatternsってやつが入ると書かれている．余(co-)がついてるのでたぶん健康によくないやつなんだろうなと思いつつ読むと，なにやらこんなカンジのようだ． タプルをレコードで定義すると，次のようになる． record _×_ (A B : Set) : Set where constructor _,_ field fst : A snd : B open _×_タプルのフィールドとしては1番目の要素であるfstと2番目の要素であるsndを持っていて，recordをopenすればこれらは普通に関数として使える． 通常，タプルを与えるような関数は最終的にタプルをコンストラクトすることになる． pair : {A B : Set} →
The Agda Challenge
This is a proof server. You can enjoy theorem proving here in Agda. Problems Recent Entries How to submit proofs. Open problem page. There are some code fragments (Definitions, Theorem and Verifier). Some problem contains 'Definitions' part. In this case, save as 'Definitions.agda'. $ agda Definitions.agda Next, save 'Theorem' as 'Theorem.agda'. This part has postulated theorems. Complete proof. $
Agda2のcodata定義 - ラシウラ
Agda2では、dataで定義したデータ型は有限で、それを利用する再帰関数も停止性が証明できないといけないけれど、codataは、停止しない再帰関数を記述することができます。 定義は、ラベルがcodataである以外、dataと同じです。以下のStream Aは、List Aと同じ構造ですが、有限である必要がないので、nil相当のコンストラクタはcodataには不要です。むしろnil相当が存在しないことで、このcodataが必ず無限であることをあらわしています。 codata Stream (A : Set) : Set where stream : A -> Stream A -> Stream A {- <=> data List (A : Set) : Set where nil : List A cons : A -> List A -> List A -} data同様に、普通の関
Agda2ことはじめ - ラシウラ
参考は http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf とAgda2添付のexamples、そしてソースコード。 一応emacsインタフェースで、コード補完(別名、証明補助)できるUIがあるのですが、自分はまったく使ってません。 一応、こういうdependently typedな言語では、式と型の区別はないようなもので、型部分でも値や関数適用ができるため、それらを合わせて項(term)として扱うのですが、そのtermの意味で式や型という語をわざと使っています。 Agda2の基本 簡単なものとして、AgdaIntroにもある、trueとfalseからなるBool型データと、その関連関数を定義しましょう。 まず、Boolデータ型 data Bool : Set where true : Bool fa
Coq/Agdaのどちらを使う？
この記事はTheorem Prover Advent Calendar 14日目の記事です。 さて、登録した時点では「Agdaが多いなあCoqかなあ」などと暢気に言っていて、また一日目のnotogawaさんは「みんなCoqのことを書くに決まってる」っぽいことをAAで言っていたわけですが、箱を開けてみたら Σ(●△●)＜Isabelleの人が一人で大半埋めてるじゃねえか！？ というわけでここではCoqとAgdaのことを書きましょう。そうしましょう。 え、CoqとAgdaのことはnotogawaさんが書いてただろって？ 細けえこたぁいいんだよ！ ・CoqとAgda、どちらを使うべき？ 好きな方を選べば良いと思うのですが、個人的な考えを挙げます。 1:性質＋証明を書くならCoqがいいです。記号処理や数学の定式化などですね。この辺りはtacticを使うという戦略がかなり効きます。ただ、これに関して
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - divipp/PandocAgda: Pandoc support for literate Agda
jstolarek.com
GitHub - myuon/agda-cate: Category Theory in Agda
ProofCafe - Schedule/ProofSummit2014
GitHub - nfjinjing/chu2: Chu2 Agda Web Server Interface
Agda copatterns (Release notes for Agda 2 version 2.3.4)
GitHub - alexandersgreen/qio-agda: The Quantum IO Monad, implemented in Agda
AOPA | The Agda Wiki
ForeignFunctionInterface | The Agda Wiki
GitHub - pi8027/lambda-calculus: A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2
An Introduction to Agda
MiniAgda Home Page