四則演算を複数行って出力出来るだけですけど、 HaxeをC++に変換して実行すると、x86_64のアセンブラを吐き出し、gccを呼んでアセンブラをアセンブルしてます。 /** * Haxeでosx用のx86_64用のコンパイラのコア */ import haxe.io.Eof; import sys.io.File; …

えーと、TAPLの3.2.5をCoqを使って、証明しようと思ってたところです。TAPLの3.2.5を証明するには、Coqで実装する方法を知らないと出来ないのでした。なので、実装方法を知らねばならず、4章の内容を知らないと出来ない事をやろうとしてますと。しかも、Coq…

論文は見つかったのですけど、英語で難しい。 ってことで、実装ないんかと探してみると、実装の論文は見つかったんですけど、実装そのものは見つかりませんでした。http://d.hatena.ne.jp/osiire/20090507http://ocaml-nagoya.g.hatena.ne.jp/yoshihiro503/2…

ムツカシイので、何が難しいのか考えてみました。プログラミング言語を数学として考える場合には、何もない状態からの数学的な体系を構築する事が必要になります。ゼロから構築するので、自由にどのように構築しても良い訳です。自由ではあるのだけど、一般…

コンパイラを作り、SML#を勉強し、コンパイラをLLVM化し、TAPLを読みつつ、Coqを勉強し、集合論を勉強し、、、疲れました。そこで、気分転換にスタックマシン的なLLVM用のコンパイラの関数ポインタをこうすればうまく行くんじゃないかなと思ってたので修正を…

面白いです。良くわからないので何回も見直してます。 ついでにと思って、「層と圏とトポス」も買ってみました。 集合がある性質を表す物の集まりなんだけど、それを色々拡張して行くと、この方が便利だ、あの方が便利だって話になって行って、圏論が産まれ…

集合はどうも、数学の基礎にあたるようです。でも、集合を把握すする前に「定義、公理、命題、定理とは何か？」を把握すると良いです。この辺の話はCoqの構文を覚えることでプログラミング言語を覚えるように覚えることができます。http://homepage3.nifty.c…

演習は、本を書いた人が学習する為に繰り返し覚えるといいよって思う所を問題として出している訳です。問題なのですぐ答えが出せる訳では有りません。答えを見ようと思えば答え乗っていれば見れば言い訳ですが、問題意識を持ってみることが大切です。演習は…

この説明をだだだっと、姉にしてみた所、倒れて「眠い。授業したらすぐに寝れる教授になれるよ。」と言われたのでした。どうも、ああ駄目だ、理解出来ないでも、話は進んで行くとなんともたまらなく眠くなるように訓練されてしまっているんじゃないかと思い…

恥ずかしい話ですが、定義と定理の違いが良くわかってませんでした。出来るだけ避けるべき存在になってました。でも、Coqをやってみて考え方が変わりました。定義とか定理とかは、typedefとかdefとかのようなキーワードであり、構造化された文章を書く為の構…

R ⊆ S1×S2×...×Sn n-ary relation n項関係 ⊆ subset of or eauql to サブセット s1∈S1...sn∈Snに対して(s1,s2...sn)がRの要素 n-ary relation 要素(s1,s2...sn)はRによって関係ずけられる 単項関係 項が１つだけの関係 S上の単項関係 S上の述語 今までは∈??…

N Nat (Natural number) 自然数 0,1,2... ホントは2重線のNです - countable set 可算集合 自然数と一対一に対応付けられる集合

{...} Enumeration 列挙 {x ∈ S｜...} Comprehensions 内包表記 x ∈ S x is element of S xはSの要素 ∅ Empty set 空集合 S ∖ T Set Minus 差集合 S ∪ T Union 和集合 UnionのU Andの反対でOrな感じ S ∩ T Intersection 積集合 共通部分,Unionをひっくり返し…

S T U Set 集合 R Relation 関係 f(x) Function 関数 x s t u Element 要素 集合と関係と関数、要素は英語でなんと言うのかまとめてみました。 関数がFunctionと、要素はElementは有名だと思います。 関係はRelationで集合がSetが繋がってない人は多いかもし…

システムを作る際には仕様書を作って実装をするわけですが、仕様書にはそれほど記号は出てきません。理由は演算子を使えないとか、使えても限りがあるからです。そのシステムを作る為の演算子を使うってことはあまり多くないのです。記号は使わずに、英単語…

Coqのような定理証明系の言語を覚えれば、理論や証明をコンピュータ上で実装してみることが出来ます。 覚えるのには時間がかかります。地道に勉強しましょう。昨日は、Coqチュートリアルをやってみました。以下のようなファイルを用意して、CoqIDEで上行った…

2.1.1で集合は標準的な記法を用いると書いているので、これが分からないんですね。標準的な方法を知らないので、分かる訳けないですね。標準的な集合の記法を覚えよう！！「プログラミング言語の基礎概念」や「プログラミング言語の基礎理論」、「論理と計算…

全体像が把握出来てないとどのくらい進んでいるのかも分からず焦ってしまいます。そんな時は、まず全体像を把握しましょう。 2.1 集合と関係と関数 2.2 順序集合 2.3 列 2.4 帰納法 集合はJavaのコレクションでいうとSetです。関係とはMapみたいなもん。関数…

まず、このような問題については檜山正幸さんの ーーー 「形式的」とは何だろう ーーー があります。http://www.chimaira.org/docs/FormalReasoning.htm形式的なモデルを使うのに慣れてないのが１つの答えです。このページを読むと形式的な文章が読みやすく…

全体像は分かって来たので理論的な所も読みたくなってきました。 2章にはTAPLで使う定義がまとめてあり、必要なときに見ればいいと書いてあります。しかし、出来れば理解したい所です。でも覚えられない。何が分からないのかが分からない状況です。辛い理由…

今日も https://github.com/ilya-klyuchnikov/tapl-scala/ を写経しました。なんで、TAPLを読んでいるのかというと、俺俺コンパイラを作る為に型理論の勉強が必要だからです。でもTAPLをすぐに読める状況ではないので何が書いてあるのかを把握する為に、実装…

内容の理解が大切で、低利定理証明系のCoqも面白いんですけど、実装の理解も大切です。とりあえず、ソースを眺めてるだけだと分からない事も多いので写経しながら、自分の好みにあわせて書き換えてみてます。Scalaのioを使ってテキストを読み込み、パーサー…

コンパイラを作るには型理論を理解しているとよくて、型理論を理解するには数学的な証明とかが出来ると良くて、数学的な証明をコンピュータ上で出来ると楽に正確に勉強出来ると思うので、Coqを勉強してます。なんとなく、勉強してる訳ではなくて必要に迫られ…

コンパイラを作るには型理論を理解しているとよいそうなのでTAPLを読んでいます。最初からまじめに読もうとすると反射的に眠くなって駄目です。難しい。大学の時の代数学とかを思い出します。大学の時に勉強した数学は苦手ですっかり忘れてしまいました。か…

最初からレジスタマシン的に一から作り直してみてます。 で、データ構造の実験段階のものは出来た感じです。 val,var,配列、構造体が出来たと。あと、OCamlの let a = 1 in let a = a + 1 in :が書き換え出来ない変数なんだけど、名前を更新して行けて便利な…