Hilbert<ヒルベルト> - 世界で一番ピュアなプログラミング言語 -Hilbertは数学における普遍妥当な論理式を機械的に導出可能とする公理系と推論法則を言語内部に構築し、実数学の諸概念を離散世界の抽象物に飛ばす機構を目指した言語です.
Programming Language Egison
Egison - プログラミング言語→ English Version Egisonとは？ Egisonは強力なパターンマッチ機能をもつ関数型言語です． Egisonを使うと，純粋に帰納的には表せないデータ，例えば，集合や，多重集合， また環や群といった代数構造などのパターンマッチを直感的に表現することができます． Egisonのその他に以下のような特徴があります． 遅延評価 インストールの方法 EgisonはHaskellを使って実装されています． EgisonはHackageのパッケージとして配布されています． Egisonをインストールするには，GHCと Cabal-installがインストールされている必要があります． Haskell Platformをインストールすれば， その両方が自動でインストールされます． Hasekll Platformをインストールしたら，コマ
Martin-Lofの 理論とそのパラドックス - あいまいな本日の私 blog
Martin-Lofの1971年の論文では、循環性がその中核を占めています。彼は、この条件があるので、彼の理論は圏論と非常に相性が良い（ご存知のように、圏論では、圏全体は圏をなし、その意味で強い循環性を持ちます）と主張しています。しかし、翌年に、Girardがこの中核部分の（もしくは現代の書き方では Type: type）からパラドックス（ブラリ-フォルティのパラドックスの一般化）が導けることを証明し、彼の夢は消えました。現在では、循環的部分を削除した、厳格な可述性に基づく依存型理論（おそらく整合的だろうと思われるもの）が、Martin-Lofの体系ということになっています。 さて、Girardのパラドックスですが、文献は Girardの論文は仏文？だったはずなので、Thierry Coquandの An Analysis of Girard's Paradox (LICS 1986)をど
等価変換システム ETI (Equivalent Transformation rule Interpreter)
ETI (Equivalent Transformation rule Interpreter) とは、等価変換プログラミングという新しいソフトウェア開発方法を実現する言語処理システムです。BASIC、C、Prologなどのように汎用的なプログラミングが可能がですが、理論的基礎に「等価変換に基づく問題解決」を採用している点が、他の言語と大きく異なります。 等価変換とは？ 等価変換とは何でしょうか。等価変換とは、ある表現が表す意味を保存したまま表現だけを変更する変換のことを言います。記号を使って書くと「解くべき問題の条件や質問を記述した表現をP、Pが表す意味をM(P)、PをP'に書き換える変換をrとするときM(P)=M(P')ならばrは等価変換である」ということになります。等価変換を知らない人が一番イメージしやすいPの具体例は連立方程式だとおもいます。このときM(P)は連立方程式の答
L'eclat des jours(2007-08-21)
_ 山口小夜子 新高恵子か山口小夜子か、というくらいに、僕にとってのカルトスターでもあったので、またひとつの時代が消えたなぁとかいろいろ感慨。 最後に観たのは、 ピストルオペラ スペシャル・コレクターズ・エディション [DVD](江角マキコ) で、最初は単なるギルドの連絡係かと思ったらところがどっこい眼が百個（というか、この映画は最初が最近の渡哲也もかくやというくらいに膨らみに膨らんで土佐衛門のようになった沢田研二が吊るされて殺されるところから始まるわけで、監督本人にとっては60年代のおとしまえかもしれないが、見てるこっちにとっては80年代の夢は枯野に枯れすすきのような物悲しさが漂いまくるセンスパワーな映画なので、山口小夜子はまさにうってつけ）。 歌と理論は良かったけれど、映画は批評も（増殖する男を誉めたりとか）撮るのもいまひとつだった（消しゴムと扉のやつは例外的に好きだが）寺山修司の映画
はじめてのにき(2007-02-24)
_ むーん ヤター Window 一覧取れたよ! これでマカーになれるかもしれない道が開けたような。 (01:31) _ ぐおお もう世界はジョブズのものになるんだと思った。 っていうかジョブスかジョブズかもわからない。 あと端末は打てるようになったけど w3m には日本語通らないからぐぐれない。 あと HHK Pro を MacBook に刺しちゃったので Thinkpad さわらなくなった。 http://d.hatena.ne.jp/atty/20070223/p1 そういえば Firefox 入れてないからえらい不便だったんですね!! Safari ってなんだこれわ! まぁ僕はいくらなんでも日常使いマシンがゴルフサバになってるのは おたがい不幸だよねーというタイミングで おやねんがんのおかねが手に入ったぞーということで、 Mac はどうせ僕には使えないだろうから Linux マシン
CafeOBJ 入門
このディレクトリで提供しているドキュメントは、CafeOBJ の初学者への手引きである。主に自然数の仕様を例題として用い、仕様記述から証明までの流れを体験してもらうことを主眼に置いている。 このドキュメントは、次のように構成されている: CafeOBJ 処理系の使い方 CafeOBJ 処理系の起動と終了方法 仕様の記述法 仕様を CafeOBJ 処理系に読み込ませる CafeOBJ の基本的な文法などの仕様の記述法 コメント モジュール ソート 輸入 オペレータ 等式 変数 定義済みモジュールの表示 項の構文解析 項の簡約 証明譜を用いた証明法 証明譜とは 組み込み述語 = 結合律の証明 交換律の証明 補足 トラブル発生時 内蔵モジュール 識別子で日本語を使う 練習問題 改訂履歴 2008-02-06 「識別子に日本語を使う」を追加した。 2007-09-25 「証明譜とは」の証明ログのダ
CafeOBJ – Algebraic Specification and Verification
Overview CafeOBJ is a most advanced formal specification language which inherits many advanced features (e.g. flexible mix-fix syntax, powerful and clear typing system with ordered sorts, parameteric modules and views for instantiating the parameters, and module expressions, etc.) from OBJ (or more exactly OBJ3) algebraic specification language. CafeOBJ is a language for writing formal (i.e. mathe
Concurrent Clean : FGRS vs. lambda calculus - lethevert is a programmer
Cleanが意味論としてラムダ計算ではなくグラフ書き換えを使っているのはなぜかということなのですが、 Functional Programming and Parallel Graph Rewriting (International Computer Science Series) 作者: M. J. Plasmeijer,Marko Van Eekelen,Rinus Plasmeijer,M. C. J. D. Van Eekelen出版社/メーカー: Addison-Wesley発売日: 1993/07/01メディア: ハードカバー クリック: 1回この商品を含むブログ (6件) を見るを見てみると（Amazonからは入手できないですが、公式サイトからpsファイルがDLできます）、 Part 4に以下のような図があります。 Functional graph rewriting |
2006-04-24
ここでは３値論理のアウトラインを書いて、前回の課題のうち「maybe, unknown, undefined とはどういう意味の値か」だけ解決する。 ３値論理 SQLでは、nullは３値論理で扱われる。３値の真理値表は以下の通り。 NOT not true false null null false true AND true null false true true null false null null null false false false false false OR true null false true true true true null true null null false true null false nullがらみの論理演算結果、例えば nullの否定はnull. true AND null は null. true OR null はtrue. など
motionExpress
what is motionExpress? motionExpressは，コンピュータ画面上のオブジェクトの動きを，主に物理法則（ニュートン力学）によって制御する専用のプログラミング言語です． motionExpressウェブデザイナーやコンピュータを駆使するアーティストなどいわゆるコンテンツクリエイターと呼ばれる人たちや，これからプログラミングを習得しようと考えている人たちがターゲットです． 昨今のコンピュータの普及率や処理能力の向上により，コンピュータがモノ作りのツールとしてではなく，メディアそのものとして活用されるシーンが増えてきています．それはパソコン上のウェブページ画面だけではなく，携帯電話やPDAなどその領域は拡大化，複雑化しています． そうした中，そのコンテンツの表現手法に「動き」を多用する場面が増えてきています．最近ではその動きも単純なものではなく，抑揚を持っ
プログラミング言語や数式はバイダイレクショナルなのだ - 檜山正幸のキマイラ飼育記 (はてなBlog)
もうモナドの話題じゃないです。けど、少し引きずってますね； モナド関連で、「左から右」と「右から左」に触れたんですけど、そのことについてです。 ヘブライ語やアラビア語の書字方向（scriptingのdirection）は、右から左に向かう横書きということです。でも、"2006"という年号や"Isac Newton"なんて人名（外国人名になります）は左から右となるので、一行のなかに「右から左」と「左から右」が混じることになります。こんな書き方をバイダイレクショナル（bidirectional）、略してバイダイと形容します。 ヘブライ／アラビア語はたいへんだなー、と思うのだけど、プログラミング言語や数式も実はバイダイなんですよね。例えば、foo(a, b); bar(x);を考えてみると： 呼び出しの時間順は、foo(a, b);→bar(x); だから「左から右」でいいですね。しかし、引数を
データ型のクレイジー計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)
sumiiさん曰く： 「積型（組）と和型（バリアント）はあるから、多項式にテイラー展開すれば√τみたいな型も考えられる」という話を思い出しました。どこで聞いたのか思い出せないのですが… R. F. C. Waltersの"Categories and Computer Science (Cambridge Computer Science Texts)"って本のChaper 4 "Data Types"に、crazy calculation と称して無限級数の計算が載っています（sumiiさんのソースとは違う気がするが）。けっこう笑えるので紹介しましょう。 項目がAである列 まず、「I + A + AA + AAA + ... って面白いよ」と同じ例。項目の型（値の集合だと思ってください）がAである列（sequence）をSとすると、方程式は： S = I + A×S （Iは空列だけからな
d.y.d.: 砦 - "Fortress" という新しい言語について
21:58 06/04/29 FLOPS 自分はFLOPSには行ってないけど （すみません(^^;）それのために来日した人と会いまくる 日でした。具体的には shelarcy さんに誘われて、Oleg Kiselyov 氏 と Andrew Pimlott 氏 と語る会 →→ Guy Steele 氏と鍋をつつく会、のコンボ。 Oleg (SXMLの人でMetaOCamlの人でZipperFSの人でetc.etc.)もGuy(CommonLisp本の人でSchemeの 人でJavaの人でetc.etc.)も自分から見れば雲の遙か上の人で。このような機会をくれた方々に 本当に本当に感謝です。 Scheme, Haskell, ... Olegさん達とは、FLOPSで発表されてた Soutei というシステムの話。 なぜだか最後の方はひたすら cut-sea さんマシンのGaucheでUnif
並行論理プログラミングとは
First Edition: 2001.7.24 Last Updated: 2001.12.27 並行論理プログラミングは、 書き換え規則に基づいて並行に記号処理を行う言語パラダイムである。 このパラダイムに属する言語を並行論理型言語と言い、 その言語で書かれたプログラムを並行論理プログラムと言う。 【栗色の文は、歴史的なしがらみを示している。】 ■ 論理プログラミングについて 論理プログラミング（logic programming） ゴール（goal）の書き換え規則の集まりをプログラムとし、 ゴールの書き換え（rewriting）によって処理を記述する計算パラダイム。 記号処理ができ、 論理変数を頼りにプログラムを宣言的に読むことができるという特徴を持つ。 【ゴールは、一階述語論理の原子論理式（atomic formula）として解釈されてきたため、 アトム（atom）と呼ばれてきた。
OBB vs AABB - Radium Software Development
iPhoneの一般修理店は予約なしでも来店できる？ 基本的には飛び込みで修理に行ってもOK iPhoneを置いていたソファにうっかりと腰かけてしまい、パネルを割ってしまった、こんな時はスマホの一般修理店へ行きましょう。画面割れは、スマホやタブレットの故障原因として非常に多いものです。予約なしで突然お店に行っても平気かしらと、不安に思う方々もいらっしゃるかもしれません。結論としては特に問題はなく、予約なしで訪問しても画面割れの修理はお願いできます。 ただし他のサービス業のお店同様、予約なしの場合、お店が混雑していると順番待ちをしなければいけないです。特に繁盛しているスマホ修理のお店だと、行列が店内で出来ており、予約なしだと、自分の順番が巡ってくるまで長時間待たされる可能性があります。平日の朝、昼なら利用客が少ない場合が多く、飛び込みでも比較スムーズに修理が頼めます。 予約は入れた方が時短に、
IT Professionals
メタソフト CTO 早川てつろう 最終回 「語りえぬこと」〜言語の限界〜とは この連載も，いよいよ最終回となった。最後に，「論考」の結びの言葉である「語りえぬものについては沈黙せざるをえない」と，プログラミング言語の関係について考えてみたい。 メタソフト CTO 早川てつろう 第11回 オブジェクトは現実世界の像だ 前回，オブジェクトと変数について話をした。今回は，このテーマを補足する意味で，ウィトゲンシュタインの「像」という概念について説明する。 メタソフト CTO 早川てつろう 第10回 オブジェクトは変数だ プログラムを作るには，どんなプログラムを作るかという設計図が必要だ。この設計図のことを通常，「詳細仕様書」や「プログラム仕様書」と呼ぶ。プログラマは，それらの仕様書に従ってプログラムを作る。 メタソフト CTO 早川てつろう 第9回 プログラミングと実行 プログラミング言語で書か
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
http://www.kt.rim.or.jp/~kbk/zakkicho/09/zakkicho0903b.html
Error
論考