弓矢の貫通力 -
12〜16世紀くらいのヨーロッパでは、プレートアーマーが流行って、騎士たちは、全身金属板の鎧を付けて戦ったと言われる。プレートアーマーの重量は、表面積と厚みと鉄の密度の積となる。人間の表面積は、2(m^2)前後で、鉄の密度が7800(kg/m^3)くらいだから、厚さ2mmとしても、重量は31.2kgという計算。実際のプレートアーマーも、これくらいの重さはあったようで、また、これ以上厚くするのは困難だったようである(Wikipediaによれば「鎧は種類にも拠るが、重量は数十キログラムにも及び、鎧だけでも20～30kg、兜や武器を含めると35kgを超えた」らしい) 一方、武器は色々あるけど、クロスボウやロングボウは、プレートアーマーを貫通することもできたらしい。百年戦争(1337〜1453)では、ロングボウを主体とするイングランドと、クロスボウを主体とするフランスの戦いで、連射性能に劣るクロス
コンピュータ以前の数値計算(1) 三角関数表小史 -
現代の三角関数計算 三角関数の値を計算する方法として、現代人が素朴に思いつくのは (1)いくつかの角度に於ける値を事前に計算しておき、一般の場合は、それを補間した値を使う (2)Taylor展開の有限項近似 の二つの方法だと思う。Taylor展開を使う場合、角度をラジアン単位に変換する必要があるので、円周率を、ある程度の精度で知っていないといけない。 コンピュータ用に、もう少し凝ったアルゴリズムが使われることもある/あったらしいけど、今のコンピュータでは、(2)の方法が使われることが多い。例えば、Android(で採用されているBionic libc)では、アーキテクチャ独立な実装は、単純なTaylor展開を利用するものになっている。 https://android.googlesource.com/platform/bionic/+/refs/heads/master/libm/upst
はじめてのCubical -
Thierry Coquandたちが、univalenceと両立する、dependent type theoryの新しいcomputationalなmodelを作ったと言っている A model of type theory in cubical sets http://www.cse.chalmers.se/~coquand/mod1.pdf これを実装した処理系は Implementation of Univalence in Cubical Sets https://github.com/simhu/cubical に置いてある。適当にcabal installとかすればインストールできる #新しい処理系なので、若干の仕様変更により、ここに書いたコードは、そのままでは動かなくなっているっぽい。面倒なので修正はしない 細かいことはわたしもよく分かってないけど、今までHoTT(homot
迷路ソルバー -
ふと、A*-アルゴリズムって実装したことなかったな、と思ったので実装してみただけ。A*-アルゴリズムが正しいことは自明でないと思うのだけど、意外とどこにも証明とかなくて、結局、原論文を読めばいいという結論に至った。 A Formal Basis for the Heuristic Determination of Minimum Cost Paths" http://fai.cs.uni-saarland.de/teaching/winter12-13/heuristic-search-material/Astar.pdf #!/usr/bin/env python #--breadth first def route_bfs(M,start,end): def next((x,y)): if x>0 and M[y][x-1]!='*':yield (x-1,y) if x+1<len(
Coqと少しの圏論が分かる人向けのhomotopy type theory(その2) -
その2。 ホモトピー群とEckmann-Hilton argument 型がweak ∞-groupoidだということが分かったので、weak ∞-groupoidに対して、ホモトピー群というものを定義する。type theory的には、ホモトピー群を定義する動機はあまりないけど、数学にinspireされて、(意味があるかどうかは分からないけど)こういうものを定義してみて、後で、natのような具体的な型に対して、ホモトピー群を計算しようという試み 普通のgroupoid Xに対して、Hom(x,x)は群になる(xはXの適当なobject)。fundamental groupoidを思い出すと、これは、空間上の点xから点xへの適当な曲線の適当な同値類の集合と見なせる。例えば、円周の場合、適当な点Oを固定すると、fundamental groupoidは、点Oから点Oへ右回り(左回り)にn周す
Coqと少しの圏論が分かる人向けのhomotopy type theory(その1) -
The HoTT Book http://homotopytypetheory.org/book/ が完成したらしいけど、どっちかというと、数学者向けに書かれてて500ページもある。homotopy type theoryで今できてることって、CoqやAgdaで書いたら、せいぜい数千行とか、そんなもんじゃないかと思うので、長すぎる気がする 一応、HoTTに関わる知識は、型理論の他に、ホモトピー論や圏論(モナドとかHaskell関連で出てくる類の知識はあまり知らなくてもいいけど、higher categoryとか教科書に書いてなさそうな話題や、モデル圏とかを知ってるといい)があって、全部真面目に勉強しようと思うと、それぞれのテーマで一冊以上の本が書ける。ただ、実際には、ホモトピー論や圏論はアイデアや視点を提供しているだけで、あくまでCoqやAgdaで書かれてる部分が重要なので、ホモトピー論や
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
