読書会。
subtype(A, S, T) = if (S, T) U {(S, T)} in
A
else let A0 = A U {(S, T)} in
if T = Top, then
A0
else if S = S1 * S2 and T = T1 * T2, then
let A1 = subtype(A0, S1, T1) in
subtype(A1, S2, T2)
else if S = S1 → S2 and T = T1 → T2, then
let A1 = subtype(A0, T1, S1) in
subtype(A1, S2, T2)
else if T = μX.S1, then
subtype(A0, [X ↦ μX.S1]S1, T)
else
fail
TD(R) = {(T,T) | T ∈ Tm }
U {(S,T 1 × T 2) | (S,T 1) ∈ R }
U {(S,T 1 × T 2) | (S,T 2) ∈ R }
U {(S,T 1 →T 2) | (S,T 1) ∈ R }
U {(S,T 1 →T 2) | (S,T 2) ∈ R }
U {(S, μX.T) | (S,[ X ↦ μX.T] T), ∈ R } ← BU(R) との違い
BU(R) = {(T,T) T ∈ τm }
U {(S,T1 × T2) | (S,T1) ∈ R }
U {(S,T1 × T2) | (S,T2) ∈ R }
U {(S,T1 → T2) | (S,T2) ∈ R }
U {(S,T1 → T2) | (S,T1) ∈ R }
U {([ X ↦ μX.T]S, μX.T) | (S,T) ∈ R } ← TD(R) の最後と違う!
の辺りでうんうん唸ってたんですが、ここだけ抜き出してもわけわからんですなw
どうにかこうにか21章突破した(ことにした)んですが、
この章はひたすら Greatst Fixed Point だの Least Fixed Point だの
induction, coinduction, suppot function, reachable…という用語が散りばめられている
定義を追いかけ続けていたような。
正月休みに振り返ろう(と日記には書いておこう)。
→
↦
\preceq
\sqsubseteq
p20
backgroud reading winskel 1993
"再帰データ型 - Wikipedia"
http://ja.wikipedia.org/wiki/%E5%86%8D%E5%B8%B0%E3%83%87%E3%83%BC%E3%82%BF%E5%9E%8B
"Recursive data type - Wikipedia, the free encyclopedia"
http://en.wikipedia.org/wiki/Recursive_data_type#Isorecursive_types
21.12 Notes にある参考文献の数が半端じゃない… ○| ̄|_
以下読書会中にぐぐったキーワードなど
その1
Interview with John W. Eaton of GNU Octave — Free Software Foundation — working together for free software
Interview with John W. Eaton of GNU Octave
Posted by Josh Gay at Aug 31, 2012 05:29 PM
This is the first in a series of interviews the FSF's Licensing and Compliance team is
doing with maintainers of free software projects who choose GNU licenses for their
work.
GNU Octave
Today we interview John W. Eaton of the GNU Octave project, which is licensed under the GNU GPLv3.
What is GNU Octave?
GNU Octave とはなんですか?
GNU Octave is a high-level interpreted language, primarily intended for numerical computations. It
provides capabilities for the numerical solution of linear and nonlinear problems, and for
performing other numerical experiments. It also provides extensive graphics capabilities for data
visualization and manipulation. Octave is normally used through its interactive command line
interface, but it can also be used to write non-interactive programs. The Octave language is quite
similar to Matlab so that most programs are easily portable.
GNU Octave は高水準インタープリター型言語 (high-level interpreted language) であり、数値計算
(numerical computation) を指向したものです。Octave は linear problem や nonlinear problem に
対する numerical solution のための capabilities を提供しています。Octave はまたデータの
visualization や manipulation のための extensive graphics capabilities も提供しています。
Octave は通常対話的なコマンドラインインターフェースを通じて使われますが、非対話的なプログラム
を書くのにも使えます。Octave 言語は Matlab にとても似ているので、(Matlab 用の)ほとんどのプロ
グラムは簡単に移植できます。
One of the goals of the Octave project is to liberate the code written for the proprietary program,
Matlab, and allow it to run in Octave with as little modification as possible.
Octave プロジェクトの目標の一つは proprietary なプログラム (Matlab) のためにコードを書くことから
解放し、最小限の変更で Octave でも実行できるようにすることです。
There is also a companion project called Octave Forge that is a collection of
collaboratively developed packages for Octave that are analogous to Matlab's toolboxes.
Octave Forge と呼ばれる companion プロジェクトもあります。これは Matlab の toolbox のような、
Octave 向けの collaboratively developed packages のコレクションです
How are people using it?
ユーザーはどれくらいいるのですか?
There are many users of Octave and their reasons are many and varied! You can read
about some of them on our wiki.
Why did you decide to release it under the GNU GPLv3?
なぜ Octave を GNU GPLv3 の元でリリースしようと決めたのですか?
Well, it was originally published under the GNU GPLv2 or any later version, and when GPLv3 came
out, I decided to upgrade.
元々は GNU GPLv2 or any later version という条件の下で配布していたのですが、
GPLv3 が世に出たので upgrade することにしたのです。
But, there were two reasons I published GNU Octave under the GPL. First, I thought it was the
right license. I wanted to make Octave free software and I didn't want someone to be able to make
a proprietary derivative of it. Second, I wanted to use GNU readline, which is also licensed under
the GPL, and I did not want to write my own command-line editing library from scratch. But the
first reason was really the more important one for me. If I hadn't liked the aims of the GPL, I
would have worked around the readline issue somehow.
しかしわたしが Octave を GPL の元で publish したのには二つの理由があります。
第一に、GPL が正しいライセンス (right licese) であると考えたからです。
わたしは Octave をフリーソフトウェアにすることを望んでいて、それと同時に
Octavve から派生したものを誰かが proprietary なものにできてしまうことを望まなかったのです。
第二に、GPL でライセンスされていた GNU readline を使いたかったからです。
ゼロから (from scratch) 自分自身のコマンドライン編集ライブラリを書き上げることは
やりたくありませんでした。とはいえ最初の理由がわたしにとってはより重要なものでした。
もしわたしが GPL を適用するのを好ましく思わなければ、
readline 問題についてなんらかの回避策をとっていたでしょう。
As a volunteer, what's the best way to get involved in developing GNU Octave?
ボランティアとして、GNU Octave の開発において get involve する最良の方法はどういったものでしょうか?
We encourage people to start out by just being around and being social with other
developers. An easy way to start is to join the maintainers' mailing lists. Find
things about Octave you don't like, and start thinking about how to fix them. Some
people spend years helping in the mailing list before they ever delve into code.
Others sometimes jump right into coding. But, in general, a good way to learn Octave
is to understand the problems other people are having with it, so being helpful in the
mailing lists not only helps Octave as a whole, but it also prepares you to be a
better Octave contributor.
just being around and being social with other developers によって
始めることをわたしたちは推奨 (encourage) しています。
始めるための簡単な方法のひとつが maintainer たちのメーリングリストに参加することです。
Octave に関してあなたが好きでないことを見つけ、
それをどのように解消するかを考えてみましょう。
自分たちが delve into code するより前にメーリングリストで何年も活動している人たちもいますし、
Others sometimes jump right into coding.
しかし一般的には、Octave を学ぶ良い方法とはほかの人たちが抱えている問題を理解することです。
ですからメーリングリストで手助けをすることは Octave に対する援助になるばかりでなく
あなたをより優れた Octave contributor にするのです。
See our FAQ for me details on how to get involved.
What are ways that people without strong math programming abilities could start helping, today?
The documentation is always in need of improvement. People can also help with the web pages,
answering questions on the mailing lists or IRC channel. Donating to the project is also always an
option!
ドキュメントは改良のために常に必要です。あなたは web page でもって help できますし、
メーリングリストや IRC で質問に答えることも助けになります。
プロジェクトに対する donating はいつでも歓迎します!
What aspects of the project do you think could use the most help?
We currently have several large projects under development including a graphical user interface,
a just-in-time compiler, and an implementation of Matlab's "classdef"-style object system.
All of these projects have a lot of room for additional contributors.
See the GNU Octave entry in the Free Software Directory for more information.
ちょっと使ってそのあと放置しっぱなしだなあ。
その2
Whiley | Three Rules for Programming Language Syntax?
Three Rules for Programming Language Syntax?
By Dave, on January 11th, 2012
I'm always pondering the question: what makes good programming language syntax? One thing occuring
to me is that many languages often ignore the HCI aspect. For me, it's a given that the purpose of
a programming language is to simplify the programmer's life, not the other way around.
わたしは常に pondering the question しています。良いプログラミング言語の構文を作るものとはなんで
しょうか? One thing occuring to me は 多くの言語がしばしば無視してしまう HCI aspect でした。
わたしにとっては、あるプログラミング言語の目的として与えられているものはプログラマーの生活(人生?)
を単純にするためのものであって、other way around ではありません。
So, I thought of a few simple rules:
そして、わたしは二、三の単純なルールを考えました
Syntax should explain. The purpose of syntax is to help explain a program to a human.
In particular, structure in the program should be made explicit through syntax.
構文は explain であるべきである。
構文の目的は人間にプログラムを説明するのを助けるためである。
特に、プログラムにおける構造は構文を通じて explicit に作られるべきである。
Syntax should be concise. The converse to (1) is that syntax should always add to the
explanation. Syntax which does not add value simply obscures the explanation.
構文は一貫したものであるべきである。
converse to (1) は、常に構文は explanation を追加すべきであるというものです。
価値を加えない構文は単なる obscures the explanation なのです。
Syntax should conform. There are many things people learn from everyday life, and we
should not force them to unlearn these things. Doing so can confuse the explanation,
especially for non-experts.
構文は conform であるべきである。日々の生活から人が学ぶことはたくさんあり、
それらのことがらを unlearn することを我々は強制すべきではない。
そういった強制をすることは、特に non-expert たちに対して
explanation を混乱させる可能性がある。
I'm sure there are plenty of others you can think of. I pick on these because I see
them being broken constantly. Let's illustrate with some of my pet peeves:
わたしは others you can think of がたくさんあると確信しています。
I pick on these because I see them being broken constantly.
Let's illustrate with some of my pet peeves:
Colons in Type Declarations?
型宣言中のコロン
There are plenty of programming languages which use colons in type declarations (ML is a classic
example). It goes something like this:
型宣言においてコロンを使っているプログラミング言語がたくさんあります。
(ML はその classic な一例です)。それは次のようなものです
fun f (0 : int) : int = ...
For me, this breaks rule (2) because those colons do not add value. The C-family of languages is
evidence that we can happily live without them. That's not to say that C-like declaration syntax
is the “one true way”; only that it demonstrates we don't need those colons!
わたしの考えるところでは、これはルール (2) を破っています。
なぜなら、ここでのコロンは価値を付加していないからです。
C-famiy のプログラミング言語はコロンなしでも問題ないことの evidence (証拠) です。
これは C のような宣言構文 (declaration syntax) が "one true way" であるということを
主張しているのではありません。そのようなコロンが必要ないことを示しているだけなのです!
Function Call Braces: To Be or Not To Be?
関数呼び出しのカッコ
Some programming languages require braces around the arguments to a function call, whilst others
(e.g. Haskell) don't. Consider this:
一部のプログラミング言語は関数呼び出しのための引数を囲むカッコが必須ですが、
必要としないものもあります (Haskell など)。次の例を考えてみましょう
(f (g h) 1 2) y 3
What can you tell about the invocation structure from this line? Not much, unless you
happen to know from memory exactly what arguments each function takes. This violates
rule (3) since functions are normally expressed with braces in mathematics.
あなたはこの行から invocation structure について指摘できますか?
Not much,
unless you happen to know from memory exactly what arguments each function takes.
数学ではふつう関数はカッコを使って表現されているのでこれはルール (3) を破っています。
Now, how about this:
ではこれはどうでしょうか
f(g(h),1,2)(y,3)
Personally, I prefer this style. However, it would be fair to say that it violates rule (2)
since the comma's are not strictly necessary. I suppose, in fact, we have a contradiction
between (2) and (3) in this case, since commas are generally used to deliniate lists in
written English.
個人的にはこちらのスタイルが好みです。しかし、これはカンマが strictly necessary でないので
規則 (2) を破っています。実のところ、わたしはこのケースでは (2) と (3) は両立しないと仮定
します。それは英語ではカンマが通常、リストを deliniate するのに使われているからです。
Why Don't we Teach Polish Notation at School?
(answer: because we don't)
なぜ学校でポーランド記法を教えないのだろうか? (その回答: 教えていないから)
Some programming languages require mathematical expressions be expressed in Polish notation
(a.k.a. prefix notation). For example, in Lisp, we write (+ 1 2) to mean 1+2. This violates
rule (3), since most people have learned mathematics at school where the usual convention applies.
いくつかのプログラミング言語は mathematical expressions が polish notation で表現されることを
要求しています。たとえば Lisp では、1+2 を (+ 1 2) のように記述します。
ほとんどの人は学校で usual convention applies な数学を学んでいるので
これは規則 (3)を破っています。
Similarly in SmallTalk, the expression 2+3*4 is equivalent to (2+3)*4 rather than 2+(3*4),
as might be expected. Again, this violates rule (3) and is particularly insidious because
it's rather subtle.
Smalltalk では、2+3*4 という式は期待されるであろう 2+(3*4) ではなく、(2+3)*4 という式と等価です。
繰り返しますが、これは rule (3) を破っていますし、
(そういった解釈をすることは) とても稀なものであるので特に insidious (油断ならないもの) です。
The point here is not to say that e.g. one notation is fundamentally better than the other.
Just that, we learn one in school, so we should stick with that.
ここでの point は、たとえばひとつの記法 (notation) がほかのものよりも fundamentally に better
であると主張することではありません。ただ単に、わたしたちはひとつのやり方を学校で学んでいるの
だから、それに従ったほうが良いということなのです。
Conclusion
結論
Well, if you made it this far, great! Hopefully there was some food for thought, and
maybe you can suggest some other examples…
Copyright c 2012 David J. Pearce - All Rights Reserved