プログラミング

Vim+Gaucheでの作業環境の設定

追記: 書き直した Vimについて→VimでのSchemeプログラミング rlwrapについて→改めてGaucheとrlwrapの連携について rlwrapコマンドとの連携

Gaucheのread-line関数で困る時

Gaucheのread-line関数は生成する文字列に行末文字を含めずに捨ててしまう。これは、chompとかchopみたいな関数をわざわざ呼び出さなくてよいという面では、うれしい。 だけど行末文字についての情報は完全に捨ててしまうので、行末文字が何だったのか(ある…

1から9を順番に使って数を作る

Knuth: Recent Newsの冒頭の写真のケーキに 2010 = 1 + 2 + 3×(4×(5+6)×(7+8)+9) と書いてある。去年は、 Did you know that 2009 is (1/2+3)*(4+5*(6*7+8*9))? とあった。 そこで1から9を順番に使って数を作るプログラムを書いてみる。

論理とカリー・ハワード対応について書いたこと一覧とメモ

「直観主義論理の「自然さ」(1) 自然演繹」 直観主義論理の自然演繹では導入則と除去則とが相補的な関係になっている。 「直観主義論理の「自然さ」(2) シーケント計算 」 直観主義論理の自然演繹体系を変形すると直観主義のシーケント計算の体系が得られる…

シーケント計算に対応する計算体系を考えてみる

「直観主義論理のカリー・ハワード対応」(と続く文章)に書いたように、自然演繹とラムダ計算との間に対応関係があった。一方、「直観主義論理の「自然さ」(2)」 「(3)」にあるように、自然演繹とシーケント計算はおおむね対応していた。 ということは、シー…

古典論理のカリー・ハワード対応での証明の書き換えと簡約

「古典論理のカリー・ハワード対応のためのラムダ計算」のつづき。

古典論理のカリー・ハワード対応のためのラムダ計算

「call/ccと古典論理のカリー・ハワード対応」では、型付きラムダ計算にcall/ccを追加して古典論理との対応づけをしたけど、公理の追加ではなく推論規則を追加する形で古典論理との対応づけをしたい。

call/ccと古典論理のカリー・ハワード対応

「直観主義論理のカリー・ハワード対応」の続き。

直観主義論理のカリー・ハワード対応

「直観主義論理の「自然さ」(1) 自然演繹」で、「A→B」を 「A→B」というのは、Aの証明があったときにBの証明ができることをあらわす。 と解釈した。これをもっと構成的な言い方にすると

書くかもしれないことのリスト

というよりも、ずいぶん昔に書こうと思ったことの断片。

オブジェクト指向の一側面: メッセージ送信と動的結合

オブジェクト指向という言葉は、使う人によって(あるいはどの点を重視して話すかによって)意味する内容が相当違ってくるので無用な混乱をまねきがち。その上「これこそがオブジェクト指向の本質だ」とか言い出すと、さらに余計な混乱を呼んだりする。 ここで…

GaucheでSMTPクライアントを書いてみる(2) STARTTLS、AUTH

すっかり忘れていたGaucheでSMTPクライアントを書いてみる(1)の続き。

浮動小数点数の2進10進変換のこと

浮動小数点数のわかりにくさの一因 浮動小数点数は難しいし何だか怪しげな感じがする。たぶん主な理由は 数値計算の難しさ 浮動小数点数演算の難しさ だと思う。でもこれらとは別に、 浮動小数点数を使う場合、ほぼ常に2進10進変換が介入している という理由…

計算機イプシロンのこと

浮動小数点数について等しいかどうかを調べる場合、普通に等値比較をおこなうのではなく、計算機イプシロンepsを使って「|x - y| / |x| < eps」とか「|x - y| / max(|x|, |y|) < eps」としなさい、という話を聞いたり読んだりしたことがある。でも何かおかし…

OpenSSLライブラリを使ってプログラミング(3) 証明書・検証

OpenSSLライブラリを使ってプログラミング(1) OpenSSLライブラリを使ってプログラミング(2) 証明書・検証についての予備知識 の続き

OpenSSLライブラリを使ってプログラミング(2) 証明書・検証についての予備知識

OpenSSLライブラリを使ってプログラミング(1)の続き。 証明書と検証に関することで、特にOpenSSL固有というわけではない一般的なことをまとめておく。付け焼き刃の知識だけど。 証明書(公開鍵証明書)とは 公開鍵と公開鍵に関する色々な情報が載っていてそれ…

OpenSSLライブラリを使ってプログラミング(1)

にわか知識 SSL……Secure Socket Layer。SSLv2はセキュリティ上の欠陥が複数見つかっているので使うべきではない。現在使われているのはSSLv3(SSL3.0)。 TLS……Transport Layer Security。IETFが標準化した規格。SSLという名前は意図的に避けたみたい。SSLとの…

c-wrapperを使う

c-wrapperを使うと、C言語で書かれたライブラリ関数をGaucheから直接呼び出すことができる。 http://homepage.mac.com/naoki.koguro/prog/c-wrapper/index-j.html ということなので使ってみる。マニュアルは、配布されているアーカイブファイルに一緒に入っ…

GaucheでSMTPクライアントを書いてみる(1)

ネットワークプログラムをまともに書いたこともなければ知識もないので、SMTPを題材にしてプログラムを書いてみる。

WEBrickを使うためのメモ

WEBrickは、HTTPサーバを簡単に作ることができるライブラリらしい。 しかし「じゃあ簡単に作ってみよう」と思ってRubyのマニュアルのWEBrickの部分を見ても、まったく要領を得ないので、使うためのメモを書いておく。