サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
買ってよかったもの
proofcafe.org
$\displaystyle{G_1=\{0^\circ,120^\circ,240^\circ\}}$ つまりG1を0°,120°,240°の、3つの角度の集合とします。 はいっ、次に角度の足し算を。 $\displaystyle{0^\circ+120^\circ=120^\circ}$ $\displaystyle{120^\circ+120^\circ=240^\circ}$ ですが、 $\displaystyle{240^\circ+240^\circ=120^\circ}$ となります。(360°=0°です。一周して480°=120°になりました。) ということで$\displaystyle{G_1}$は角度の足し算$\displaystyle{+}$に関して群となります。 $\displaystyle{+}$ $\displaystyle{0^\circ}$ $\displa
ここでは、記号「∀」と「∃」の意味について解説していきたいと思います。 ところで、この記号→「∀」はすっごく見たことがあると思います。ほら、よく顔文字に使われている(笑) m(≧∀≦)m←こんなカンジ 確かに「∀」は笑った時の口の形に似ているので、笑顔系の顔文字によく使われたりしています。 メールが大好きな方には馴染み深い記号「∀」ですが、この記号の意味を知っている人は案外少ないのでは・・・ 数学記号はいろいろな形があるので、本来の目的に反して、顔文字の方により多く使われる・・・悲しい事実です(?) さてさて、前置きはそのくらいにしておきましょう。 記号「∀」は、アルファベットのAを逆にした記号で、「全ての」という意味になります。ALLの頭文字をとったものです。 記号「∃」は、アルファベットのEを逆にした記号で、「少なくとも一つ存在する」という意味になります。EXISTの頭文字をとったもの
proofcafe.org/~yoshihiro503
ツッコミは随時歓迎 コメントも歓迎 Coqを三行で Coqはプログラミング言語(関数型言語) Coqは仕様を書いて証明できる言語 つまり仕様が証明されたプログラミングがかける Coqはプログラミング言語 たとえばこんなん Fixpoint map{A B:Type}(f: A->B)(xs: list A):= match xs with | [] => [] | x :: xs => f x :: map f xs end.
単純型付きラムダ計算(Simply Typed Lambda-Calculus, STLC)は、 関数抽象(functional abstraction)を具現する、小さな、核となる計算体系です。 関数抽象は、ほとんどすべての実世界のプログラミング言語に何らかの形 (関数、手続き、メソッド等)で現れます。 ここでは、この計算体系(構文、スモールステップ意味論、 型付け規則)とその性質(進行と保存)の形式化を、 これまでやったのとまったく同じパターンで行います。 (扱うためにいくらかの作業が必要になる)新しい技術的挑戦は、 すべて変数束縛(variable binding)と置換(substitution)の機構から生じます。 STLC は基本型(base types)の何らかの集まりの上に構成されます。 基本型はブール型、数値、文字列などです。 実際にどの基本型を選択するかは問題ではありま
群「集合論」の知識を前提としていますFollow @tepika_math二項演算子演算子に関して閉じている半群単位元と逆元群と代数学群の位数三角形の回転部分群群の生成巡回群元の位数集合と元との演算1正規部分群剰余類剰余群同型と準同型戻る
#ProofSummit 2014 概要 定理証明支援系(Coq,Agda,Isabelle/HOL,ACL2などなど)や自動証明器などを中心に集まるお祭りです。 日時: 2014年09月06日(土) 場所: 名古屋大学 多元数理科学棟 109 参加費: 無料 参加登録: ProofSummit 2014 - Partake Twitterハッシュタグ: #ProofSummit 持ち物: おやつ、(電源タップ)、(PC) プログラム 時刻 発表者(敬称略) 所属 内容
Calculus of Construction on Web ヘルプ Powered by CoqInCoq, js_of_ocaml, and Coq
結論 最強のプログラム検証器 最強の関数型言語 最強のプログラム検証器 Coqは最強の表現力を持つ仕様記述言語を使う 仕様記述言語は検証したいこと を記述するための言語 表現力は検証器によって全然違う 表現できる範囲が、検証器の限界 Coqのそれは高階述語論理 ← 最強 最強のプログラム検証器 Coqを使うためにはPhDが必要? 高校生でも練習すればできる (c.f. プログラミングCoq) 最強のプログラム検証器 証明を人間が与えるのが大変? タクティックによる自動化はOCamlでいくらでも可能 型チェッカはタクティックと独立なので安全 既にomegaなどの自動証明アルゴリズムを実装したタクティックあり 最強の関数型言語 Coqは(型の表現力が)最強の関数型言語 型の表現力が最強 型推論は完全ではない 停止性は保証しなければならない 注意: ここでの関数型言語とは (ラムダ計算を基礎とし
前回は外積というものを紹介しました。 しかし、外積の計算は複雑なだけで、とても分かりにくいのでは・・・? そこで今回は、外積というベクトル量が一体何を表しているのか説明します(^o^)/ まず、ベクトルの外積のノルム(長さのこと)は、一体どうなっているでしょうか? とりあえず、そこから見ていきましょう。 実は、ベクトル$\displaystyle{\vec{a},\vec{b}}$の外積のノルムは 二つのベクトルのなす角度を$\displaystyle{\theta}$として、 $\displaystyle{\|\vec{a}\times\vec{b}\| = \|\vec{a}\| \|\vec{b}\| \sin\theta}$ となっています(余裕のあるのある人は、実際に計算して確かめてください)。 これって、高校数学の知識でも分かると思いますが、平行四辺形の面積ですよね? 辺の長さ
proofcafe.org/~keigoi
コースの最初のパートで用意した数学的道具立てを、 小さなプログラミング言語 Imp の理論の学習に適用し始めています。 Imp の抽象構文木(abstract syntax trees)の型を定義しました。 また、操作的意味論(operational semantics)を与える評価関係 (evaluation relation、状態間の部分関数)も定義しました。 定義した言語は小さいですが、 C, C++, Java などの本格的な言語の主要な機能を持っています。 その中には変更可能な状態や、いくつかのよく知られた制御構造も含まれます。 いくつものメタ理論的性質(metatheoretic properties)を証明しました。 "メタ"というのは、言語で書かれた特定のプログラムの性質ではなく言語自体の性質という意味です。 証明したものには、以下のものが含まれます: 評価の決定性 異なっ
線形代数学行列やベクトルの知識が前提です。⭐️マークのページは難易度の高いページですので、読み飛ばしても構いません。Follow @tepika_math最初に内積内積とノルム外積外積の意味領域と集合一次結合一次結合の意味するもの一次独立一次独立の意味するもの線形空間線形空間の例基底線形空間の次元基底のとりかえ次元について線形部分空間⭐️抽象ベクトル空間行列とは転置対称行列と直交行列行ベクトル・列ベクトル行列によるベクトルの変換写像とは戻る
プログラミング言語Coqには、ほとんど何も(ブール型や数値型すら)ビルトインされていません。その代わりCoqには、新しい型やそれを処理するための強力なツールが用意されています。 まず最初はとても簡単なサンプルから始めましょう。次の定義は、Coqに対して、新しいデータ型のセット(集合)である'型'を定義しています。その型はdayで、要素はmonday、tuesday...などです。その定義の1行は以下のようにも読めます。"mondayはday。tuesdayはday"といった具合です。
Benjamin C. Pierce Chris Casinghino Michael Greenberg Vilhelm Sjöberg Brent Yorgey with Andrew W. Appel, Arthur Chargueraud, Anthony Cowley, Jeffrey Foster, Michael Hicks, Ranjit Jhala, Greg Morrisett, Chung-chieh Shan, Leonid Spesivtsev, and Andrew Tolmach
メインメニューメールはこちらへ↑↑↑
ソフトウェアの基礎(beta)¶ 本ドキュメントは実験中のものです。 安定板は http://proofcafe.org/sf/ を参照してください。 epub版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.epub mobi版: http://proofcafe.org/sf-beta/software_foundation_1.0.2.mobi Contents:
はいっ!゜☆。.:* 来ましたね!!! 今回は一次独立というものを解説します。 「一次独立」とは、線形代数学をやっていく上で、とても重要な用語です!! 是非とも、十分に理解しておいてくださいm(_ _)m 一次独立は線形独立と呼ばれることもあります。 また、一次独立でないとき、一次従属または線形従属と言います。 今回は、いきなり定義から入っちゃいます☆ ベクトルの組$\displaystyle{v_1,v_2,\cdots,v_n}$に対し、 $\displaystyle{k_1v_1+k_2v_2+\cdots+k_nv_n=0}$ となるのは$\displaystyle{k_1=k_2=\cdots=k_n=0}$のときのみに限るとき、 ベクトルの組$\displaystyle{v_1,v_2,\cdots,v_n}$は一次独立であるという。 恐らく、定義だけでは『なんのこっちゃ??』
第16回 TAPL-nagoya 勉強会 日時: 2013年8月17日 14:00 - 17:00 場所: 名古屋大学(の予定) 参加登録 概要:10章 ハッシュタグ: #taplnagoya 第15回 TAPL-nagoya 勉強会 日時: 2013年7月20日 18:00 - 20:00 場所: 名古屋大学 東山キャンパス 多元数理科学棟 1階109号室 参加登録 概要:5, 6, 7章の理論部分流し読み ハッシュタグ: #taplnagoya 第14回 TAPL-nagoya 勉強会 日時: 2013年6月16日 14:00 - 17:00 場所: 名古屋大学 東山キャンパス 多元数理科学棟(旧理1号館)3階309号室 参加登録 概要:5, 6, 7章の予定 ハッシュタグ: #taplnagoya 7章の実装 OCaml Ruby prolog coq 第13回 TAPL-nagoy
2011/11/8位相:「触点」追加線形代数:「行列とは」追加線形代数:「転置」追加線形代数:「対称行列と直交行列」追加 2011/6/11公理的集合論:「ZFCの公理系」追加公理的集合論:「公理とは?」追加公理的集合論:「ペアノの公理」追加公理的集合論:「定義とは」追加公理的集合論:「命題・述語」追加公理的集合論:「はじめに」追加位相:「抽象的な内部・外部・境界」追加位相:「内部・外部・境界」追加位相:「内点」追加位相:「近傍」追加位相:「距離誘導位相」追加位相:「集合間の距離」追加線形代数学:「抽象ベクトル空間」追加線形代数学:「線形部分空間」追加線形代数学:「次元について」追加線形代数学:「基底のとりかえ」追加線形代数学:「線形空間の次元」追加線形代数学:「基底」追加線形代数学:「線形空間の例」追加線形代数学:「線形空間」追加線形代数学:「一次独立の意味するもの」追加線形代数学:「一
#ocamltter ocamltter は ターミナルで動作する Twitter クライアントです。OCamlの対話環境を使って動作するのでOCamlの関数を利用することができます。または対話的にオリジナル機能やボットなどを開発することができます。 ocamltterで日常的にOCamlに触れることによって、自然に関数型言語(ML)の技術を身につけることができるでしょう。 #リポジトリ http://github.com/yoshihiro503/ocamltter #API Document (ocamldoc) http://yoshihiro503.github.com/ocamltter/ #インストール方法 その1: OPAMを使う - opam install ocamltter #インストール方法 その2: ソースからインストール ## 必要要件 - OCaml >= 4.
機械がチェックした証明においては、細部の一つ一つの正しさが確認されています。 これが巨大な証明記述にもなります。 幸い、Coqは証明探索メカニズムと決定手続きを持っていて、 それにより証明の小さな部分を自動合成することができます。 自動化は設定を適切に行えば非常に強力です。 この章の目的は自動化の扱い方の基本を説明することです。 この章は2つの部分から成ります。 第一部は証明探索("proof search")と呼ばれる一般的メカニズムに焦点を当てます。 簡単に言うと、証明探索は、証明が終わるまで、 単純に補題と仮定を可能なすべての方法で適用してみようとします。 第二部は決定手続き("decision procedures")について記述します。 それらは、Coqの論理の特定の断片についての証明課題を解くことを得意とするタクティックです。 この章の例には、自動化の特定の側面を示す小さな補題
#Coq to Scala English ##概要 Coq2ScalaはCoqのExtraction機能に関する拡張です。 Coq2ScalaはCoqで定義されたアルゴリズムをScalaと連携しJVM上で高速に動作させることを可能にします。 開発者: 今井宜洋(ITプランニング)、姜帆(東京大学 情報理工学系研究科) ハッシュタグ: #coq2scala リポジトリ: http://bitbucket.org/yoshihiro503/coq2scala ##アルゴリズム Mprime_annot ##ダウンロード こちらからパッチをダウンロードできます: https://bitbucket.org/yoshihiro503/coq2scala/downloads ##インストール 1. 上記から差分ファイルをダウンロードし、対応するcoqのソースコードもCoq本家から取得します。 2.
Symbols_J:概要 Preface_J:前書き 前書き 概要 実際の学習について 章間の依存関係 学習者に要求される知識的前提 Coqについて 学習に必要なもの 教材となるCoqファイルの入手方法 練習問題について 推奨書籍 教育関係者へ Basics_J: 関数プログラミングとプログラムの証明 列挙型 曜日の表し方 ブール型 関数の型 数値 簡約を用いた証明 introsタクティック 書き換え(Rewriting)による証明 Case分析 Caseへのネーミング 帰納法 形式的証明と非形式的証明 証明の中で行う証明 さらなる練習問題 Lists_J: 直積、リスト、オプション 数のペア 数のリスト リストを使ったバッグ リストに関する推論 お小言 リスト上の帰納法 SearchAbout リストについての練習問題 (1) リストについての練習問題 (2) オプション apply タ
Login / Get an account Logout viewedithistorydiscuss Front Page ProofCafe ー 名古屋Coq勉強会 ー の情報は、以下のリンクを参照してください。 https://proofcafe.connpass.com powered by gitit , hosted on proofserver
次のページ
このページを最初にブックマークしてみませんか?
『http://proofcafe.org/』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く