証明プログラミング超入門
東京大学 松尾研究室が主催する深層強化学習サマースクールの講義で今井が使用した資料の公開版です． 強化学習の基礎的な概念や理論から最新の深層強化学習アルゴリズムまで解説しています．巻末には強化学習を勉強するにあたって有用な他資料への案内も載せました． 主に以下のような強化学習の概念やアルゴリズムの紹介をしています． ・マルコフ決定過程 ・ベルマン方程式 ・モデルフリー強化学習 ・モデルベース強化学習 ・TD学習 ・Q学習 ・SARSA ・適格度トレース ・関数近似 ・方策勾配法 ・方策勾配定理 ・DPG ・DDPG ・TRPO ・PPO ・SAC ・Actor-Critic ・DQN（Deep Q-Network） ・経験再生 ・Double DQN ・Prioritized Experience Replay ・Dueling Network ・Categorical DQN ・Nois
定理証明支援の紹介 - Qiita
目的 定理証明支援とは何かと現状の整理。 定理証明支援とは 定理証明支援とは数学の定理を自動で証明することではなく、ステップバイステップでコンピュータに命令を送り、数学の定理を証明するのを助けるシステムである。 支援だから意味ないということでなく、最近の数学の証明は長くなり証明の検証が難しいのを助ける意味がある。定理証明支援の意義についてはこちらが詳しい。 また、信頼性が求めらる難しいアルゴリズムの検証、たとえばTLS(暗号通信)やRaft(分散合意アルゴリズム)のサーバーに利用されつつある。 ここでいう定理は大げさなものだけでなく、$1+1=2$、$0*何か=0$、$a*b=b*a$といった簡単なものを証明しながらどんどん積み上げていく。通常のプログラムと違うのは証明であるので使用する変数が整数ならそのすべての値について成り立つ定理を証明する。 定理を証明するのに使うツールは下記である。
Agda を使ってみる - 再起動中...
Proof Summit に参加している。 Agda を初めて使う。 インストールは 掲示板で紹介されていた ここ を参照した。 Ubuntu 8.04 LTS では… sudo apt-get install agda-mode sudo apt-get install agda-stdlib で使えるようになった。 yoshihiro503 さんのサイトを参考に実行した。 ./src/myFirstAgda に hello.agda を用意。 module hello where open import IO main = run (putStrLn "Hello, あぐだ World!") ここで、C-c C-l で型チェック、C-c C-x C-c でコンパイル。 ./hello ができるので、実行できる。 文字コードは、UTF-8 だ。 文字コードが UTF-8 のため、数学の記
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
安全かつ柔軟な依存型 -
この記事はTheorem Proving Advent Calendar 2011の1日目の記事です。 今日は Agda2 というプログラミング言語を用いて、依存型を用いることで絶対的な安全性と Haskell や OCaml などでは(通常の方法では)実現できない柔軟さのどちらも持つプログラムを記述できるということについて書きます。 この記事は主に、普段動的型付けのプログラミング言語を使っていて、静的型付きの言語では自分の意図したものを十分に表現できないと考えている人を対象読者としています。 依存型とは 型に依存する型や、値に依存する型を作れる型のことです。 例えば、値に依存する型を用いることで型レベルでサイズが与えられているリストを作ることが可能です。 また、リストの結合関数は長さ a のリストと長さ b のリストを取り、リスト a+b のリストを返すというような型を持つことになります
Gre BattleSouls quite WarBirds Dogfights 2016 fore
However, they are not at all obvious. They have many unlockable machines, many options and levels and a powerful online multiplayer mode. Are you looking for quickness for this impure polyphony? This limited amount can abandoned be a cube or a ball. organization continues even though facility is installed. Now that you comprehend the increase of Asgard, you are ready to conquer it. 10p two mmo pla
Agda - Wikipedia
agda2による証明の抜粋 Agda（アグダ）は、定理証明器、すなわち数学的な証明を検証するコンピュータプログラムであり、ペール・マルティン＝レーフの型理論の一種における構成的証明構築のための対話的システムである。機能的には、依存型をもつ関数型プログラミング言語であるともみなすこともできる。1990年代よりチャルマース工科大学で主に開発されている。 他の定理証明支援系ではスクリプトによって「タクティク」(tactic)を指定して証明を操作するのに対して、Agda では証明を項として表し直接操作するというアイデアに基づいている。言語はデータ型や case式、シグネチャやレコードといった一般的なプログラミング構成概念をもつ。Emacsインターフェイスを使って対話的にコードを作成できるほか、直接コードをコンパイルする処理系の開発も進んでいる。 Agda[編集] Agda は当時チャルマース工科大
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
A Simple Introduction to Agda