POSTD | ニジボックスが運営するエンジニアに向けたキュレーションメディアPOSTD は、ニジボックスが運営する、エンジニアに向けたキュレーションメディアです。ニジボックスはWebサービスの企画、制作、開発、運用を一貫して担うリクルートの100%子会社です。 リクルートグループのオンラインサービスをはじめ、様々な業種・業界・業態のサービス開発を行っております。
Coqと少しの圏論が分かる人向けのhomotopy type theory(その1) -
The HoTT Book http://homotopytypetheory.org/book/ が完成したらしいけど、どっちかというと、数学者向けに書かれてて500ページもある。homotopy type theoryで今できてることって、CoqやAgdaで書いたら、せいぜい数千行とか、そんなもんじゃないかと思うので、長すぎる気がする 一応、HoTTに関わる知識は、型理論の他に、ホモトピー論や圏論(モナドとかHaskell関連で出てくる類の知識はあまり知らなくてもいいけど、higher categoryとか教科書に書いてなさそうな話題や、モデル圏とかを知ってるといい)があって、全部真面目に勉強しようと思うと、それぞれのテーマで一冊以上の本が書ける。ただ、実際には、ホモトピー論や圏論はアイデアや視点を提供しているだけで、あくまでCoqやAgdaで書かれてる部分が重要なので、ホモトピー論や
京大マイコンクラブが教える絶対に失敗しない言語の選び方
京大マイコンクラブが教える絶対に失敗しない言語の選び方！！！ 4月から始まる新しい生活,新しい環境…… そんな不安と期待が入り交じる環境を支えてくれるのは…… やっぱり新しいプログラミング言語ですよね！！！？？？ 下の質問に答えて、キミにピッタリのプログラミング言語と4月からの新しい生活を過ごしてくれ！！！！ 各言語をクリックするとその解説ポエムが読めます。 ⚠ このチャートはエイプリルフール企画として作成されたものです (> < )。……質問がよくわからない時はNoを選びましょう！ Tweet ノートパソコンの選び方版はこちら
青春→鯖鰆みたいなやつ - アスペ日記
今日、こんなツイートを見かけました。 娘１のクラスの寄せ書き、「楽しかったよ」「また会おうね」が多い中、キラリとひかる名文発見。「青春って魚編をつけると鯖鰆（サバサワラ）って読めるよね。似たような熟語を見つけたら教えて」By 町田高史(仮名) 彼が無事に社会に適応できますように。— 藤川ｵﾚﾝｼﾞｰﾅ (@Forangina) 2017年3月21日 ぼくもこういうのは大好きです。 （社会に適応できているかどうかは微妙なところです） それで、こういうのを探してみることにしました。 漢字の構造については、漢字構造情報データベース（CHISE）というものがあります。 （かなりの労力がかかっていると思われるデータベースです。作られた方に感謝します。） 今回は、これを使わせていただきます。 % git clone http://git.chise.org/git/chise/ids.git この中の
マリオメーカーはチューリング完全だった【万能計算機】
マリオメーカーがチューリング完全であることの、数学的な証明に成功しました。ルール110セルオートマトンと、cyclic tag system（循環タグシステム）をコース内で再現しました。youtube 版（英語字幕付）：https://www.youtube.com/watch?v=hd0EtsTUbmg マリオメーカー計算機マイリス：mylist/53578200コースID：[ルール110] 63FA-0000-02C4-B1CA [cyclic tag system] FA62-0000-02C9-A346マリオメーカーブックマーク：supermariomakerbookmark.nintendo.net/profile/yos1up連絡先：@yos1up (twitter)
形式手法 - Wikipedia
Z言語を使った形式仕様記述の例 形式手法（けいしきしゅほう、英: formal methods）は、ソフトウェア工学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である[1]。ソフトウェアおよびハードウェア設計への形式手法の適用は、他の工学分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている[2]。 形式手法は理論計算機科学の様々な成果を基盤として応用したものであり、数理論理学、形式言語、オートマタ理論、プログラム意味論、型システム、代数的データ型などを活用して、ソフトウェアおよびハードウェアの仕様記述とその検証を行う[3]。 分類[編集] 形式手法はいくつかの水準で使用可能である: 水準0 形式仕様記述を行い、プログラム自体を非形式主義的に行う。「軽い形式手法」と呼ぶ。費用対効果が早く得るこ
Alloyを使って有限群を調べてみる - ashiato45の日記
Alloyはモノを抽象的に記述したり、それらの関係を数学で言うところの「関係」でもって記述する言語です。 さらに、そこで記された制約を満足する例を見つけたり、制約に対する反例を見つけたりするための解析器がついてます。 プログラムの仕様をこれで記述して、それに対して見落しがないかを探すのに便利みたいです。 公式サイトhttp://alloy.mit.edu/alloy/の記述を引用すると、 Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching net
計算機イプシロンのこと - 再帰の反復blog
浮動小数点数について等しいかどうかを調べる場合、普通に等値比較をおこなうのではなく、計算機イプシロンepsを使って「|x - y| / |x| < eps」とか「|x - y| / max(|x|, |y|) < eps」としなさい、という話を聞いたり読んだりしたことがある。でも何かおかしい気がする。それ以前に計算機イプシロンが何なのかもよくわからない。なので、そのことについてメモにまとめる。 浮動小数点数の等値判定の仕方 計算機イプシロンの定義 計算機イプシロンの定義:その1 計算機イプシロンの定義:その2 定義1と定義2の混同 (定義2の計算機イプシロンの意味) 浮動小数点数の等値判定に計算機イプシロンを(どう)使うべきか 浮動小数点数の等値判定はどのようにすべきか 浮動小数点数の等値判定の仕方 文章が長いので、浮動小数点数の等値判定の仕方を先に書いておく。 適当な定数Cを取って で等
自己複製 - Wikipedia
この記事には参考文献や外部リンクの一覧が含まれていますが、脚注による参照が不十分であるため、情報源が依然不明確です。適切な位置に脚注を追加して、記事の信頼性向上にご協力ください。（2024年2月） 自己複製（じこふくせい、英: Self-replication）とは、何らかの事物がそれ自身の複製を作る過程である。細胞は適当な条件が整うと、細胞分裂による複製を行う。細胞分裂において、DNAが複製され、生殖に際してはそれが子に転送される。ウイルスも複製されるが、細胞に感染して細胞の持つ生殖機構に指令を出すことでのみ複製可能である。コンピュータウイルスは、コンピュータに備わっているハードウェアやソフトウェアを使って複製を作る。ミームは人間の精神や文化を一種の生殖機構として利用して複製を作る。なお、自己複製子（じこふくせいし、英:self-replicator）とは遺伝子やミームなど、自らの複製を
最適化問題 - Wikipedia
最適化問題（さいてきかもんだい、英: optimization problem）とは、特定の集合上で定義された実数値関数または整数値関数についてその値が最小（もしくは最大）となる状態を解析する問題である[1]。こうした問題は総称して数理計画問題（すうりけいかくもんだい、英: mathematical programming problem, mathematical program）、数理計画とも呼ばれる[1]。最適化問題は、自然科学、工学、社会科学などの多種多様な分野で発生する基本的な問題の一つであり、その歴史は18世紀の変分問題に遡る[2]。1940年代に線型計画法が登場して以来、理論的な研究や数値解法の研究が非常に活発に行われ、その応用範囲はいろいろな分野に拡大されていった[1]。実世界の現象の数理的な解析に関わる問題や抽象的な理論の多くをこの最適化問題という一般的なくくりに入れるこ
鳩の巣原理特集 - 問題解決の宝石箱
Competitive Programming Advent Calendar 2016 23日目の記事です。 鳩の巣原理と、競技プログラミングでの使われ方を紹介します。 鳩の巣原理とは 昔々あるところに、5羽の鳩がおりました。彼らをすべて巣箱に入れたいのですが、あいにく巣は4つしかありませんでした。 すると以下の図のように、どこか1つの巣には2羽以上の鳩が入ってしまいます。 適当な入れ方をすると、2羽より多い巣があったり、空の巣があるかもしれません。でも、どんな入れ方をしても「どこかの巣には2羽以上」入ることが保証されます 。 一般に n 羽の鳩を m < n 個の巣にいれるとき、どこか 1 つの巣には鳩が2羽以上入ります。 更に一般化。巣に入っている鳩の最大数を最小化しようとすると、各巣になるべく均等に鳩を配る形になります。 このとき、鳩の数の最大値は *1 となり、これが最大値の下限
apollo11号のソースコードを読みつつ - aerith7’s blog
これはなに？ はじめに AGCあれこれ Temporary I HOPEHOPEHOPE ASTRONAUT NOW LOOK WHERE YOU ENDED UP ふと気になりました いい時代ですね 1201&1202エラー なにそれ？ カ、カルマンフィルターだー！！！ カルマンフィルターの開発経緯 その他面白コメントアウト集 TRASHY LITTLE SUBROUTINES（つまんないサブルーチン） NUMERO MYSTERIOSO（神秘の数字） OFF TO SEE THE WIZARD COME AGAIN SOON HONI SOIT QUI MAL Y PENSE（悪意を抱く者に災いあれ）、NOLI ME TANGERE（私に触れるな） PINBALL_GAME_BUTTONS_AND_LIGHTS.agc おわりに 反省 参考文献 これはなに？ この記事はeeic Adv
while my_mcmc: gently(samples) - Bayesian Deep Learning
Variational Inference: Bayesian Neural Networks 2016-2018 by Thomas Wiecki, updated by Maxim Kochurov Original blog post: https://twiecki.github.io/blog/2016/06/01/bayesian-deep-learning/ Current trends in Machine Learning There are currently three big trends in machine learning: Probabilistic Programming, Deep Learning and “Big Data”. Inside of PP, a lot of innovation is in making things scale us
有理数とか有限体とかのはなし - Qiita
一部間違いがあります、本文中でも明記しましたが最初の終了条件はInt を覆っていません。 最後に訂正したバージョンとより厳しいquickCheck の結果も載せておきました。 Haskell Advent Calendar 2016 の10日目です。 去年は眺めているだけだったので今回枠取れたの嬉しいです！ レベル分け的にはAdvanced Beginner の一人が同じくらいのレベルの人に向けて書いてるつもりです、やや内容に初等整数論が含まれます。 あわよくばより詳しい人にトンテンカンカンと直していただきたい感じですが。 モチベーション 電卓などで(1/3) の計算をした後、答えに3 を掛けたことがある人、そしてそのとき1 に戻らなかった経験ある人もきっと多いことだと思います。 今回の話はそれにちょっと関係している、かもしれません。 今回は体を取り上げます、体と言うのはいわゆる四則演算に
Coq で圏論：背景と普遍性について - Qiita
暇つぶしに、 Coq 上で Setoid ベースの構成的な圏論をやっている。 どういうことかというと、 普通の圏論における局所小(locally small)な圏を基準に、 普通の圏論における「集合」を Setoid で置き換えて、 なるべく exists を使わないで構成的に圏論を展開 という感じ。 構成的にしている理由 「性質 P を持つ Ｘ が存在する」をそのまま exists X, P(X) みたいに書くのではなくて、存在するなら実際に作ってみせよ、というスタンスです。 命題の形にしてしまうと、存在するという事実から実体を取り出せず、圏論的な理論展開をほぼ全部命題ベースで行なわなければならなくなります。 そうしてしまうと、 Coq 上のデータが実はある種の圏論的な構成として得られるのでしたーという時に、それまで展開していた(Coq 上での)圏論の資産を直接利用できません。 要するに
人工知能の歴史 AIを如何にして達成しようとしたか - HELLO CYBERNETICS
※めちゃくちゃ長いです。一連の流れで読むと理解が深まると思います。自身の復習のためにも書き下しました。個々の章で完結しているので、それぞれ別の記事としても掲載しています。 近年は人工知能ブームが到来し、人工知能というワードを当たり前のように使う時代がやってきました。情報技術を学んでいる人にとって人工知能は、情報処理を効率的に行う素晴らしい技術の一つとして認識できるかと思います。一方で、技術的話題にあまり興味がない人にとっては、人工知能というワードに対して各々の解釈をして、時には誤解のような意見も見受けられます（人工知能の全容がハッキリしないうちは誤解というのはあまりにも強すぎる言い方ですが）。 人工知能がどういうものであるのかを知るには、人工知能を技術的にいかにして達成しようとしたかの歴史を知ることが一番であると思います。 ここでの記事の目的は技術的な観点からの人工知能について説明すること
A tutorial on linear prediction and Levinson-Durbin
1 Linear Prediction and Levinson-Durbin Algorithm Cedrick Collomb http://ccollomb.free.fr/ Copyright © 2009. All Rights Reserved. Created: February 3, 2009 Last Modified: November 12, 2009 Contents 1. Description of Linear Prediction...............................................................................................1 2. Minimizing the error ..............................................
コンパイル中にコンパイルする「コンパイル時Cコンパイラ」をつくった話 - kw-udonの日記
僕は先日、「コンパイル時Cコンパイラ」なるプログラムをつくって、公開した。 「コンパイル時Cコンパイラ」とは、コンパイルするとC言語プログラムのコンパイルが行われるというようなC++プログラムである。 C++のコンパイル中に C言語プログラムのコンパイルを行う、 "コンパイル時Cコンパイラ"をつくりました #ELVMhttps://t.co/kKiLU3rLFX— うどん (@kw_udon_) 2016年11月18日 自分で書いておいてなんだが、「なんのこっちゃ」という感じではある。(ちゃんと記事中で説明する。) 実際、変なプログラムではあるのだが、とても嬉しいことに多くの人に面白がっていただき、予想だにしなかった大きな反響をいただいた。 Hacker Newsで1位になったり、LLVMの公式ブログで紹介されたり、果てはC++の作者であるBjarne Stroustrupにも言及されるに
PRML - 朱鷺の杜Wiki パターン認識と機械学習 - ベイズ理論による統計的予測
パターン認識と機械学習 - ベイズ理論による統計的予測† This is a support page for the Japanese edition of "Pattern Recognition and Machine Learning" authored by C. M. Bishop. 本書は，Christopher M. Bishop 著「Pattern Recognition and Machine Learning」の日本語版です．上下2巻の構成です． パターン認識や機械学習の各種のアルゴリズムや背後の考えについて，ベイズ理論の観点から解説した教科書です． 基礎的な線形モデルから，カーネルトリック，グラフィカルモデル，MCMCなどの発展的な話題までをバランス良く収録しています． 数式による形式的な記述だけにとどまらず，豊富なカラーの図による直観的な説明もなされています． 本
NumPy・SciPyを用いた数値計算の高速化 : 応用その1 - Qiita
対象 Python及びNumPy初心者に向けて書いています. 「C言語は使えるけど最近Pythonを始めた」とか「Pythonらしい書き方がよくわからない」に該当する物理系の数値計算を目的とした方には特に有用かもしれません. また, 自分の不勉強のために間違った記述があるかもしれません. ご容赦ください. あらまし 内容はNumPyを用いた数値計算の高速化 : 基礎のつづきです. ndarrayのユニバーサル関数や演算を用いて可能な限りforループを使わずに基礎的な数値計算を実装していきます. 今回からSciPyも仲間に加わります. 以下ではNumPy・SciPyの関数の詳しい実装についてはあまりコメントしていないので, わからないことがあったら是非リファレンスを読んでみてください. 言わずもがな, 車輪の再発明をしないことがとっても大事です. 微分 物理の基礎方程式には微分がつきものです
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
