タグ

ProgrammingとLogicに関するTaKUMAのブックマーク (5)

  • LiLFeS

    LiLFeSは、型付き素性構造 を用いたプログラミング言語です。特徴としては、 素性構造が組み込みデータとして使える。--- Prolog のような論理型言語 で,素性構造を組み込みデータ構造とするプログラムを簡単に書くことができ ます。 処理が高速。--- 処理が重くなりがちな素性構造の「単一化」を高速に処理 することができます。 強力なデータベース機能を持つ。--- 素性構造をキーとするデータベースを 利用することができます。 C++言語用のライブラリを提供。--- 型付き素性構造を扱うプログラムを C++ 言語で簡単に実装することができます。 などが挙げられます。LiLFeSが提供するC++言語用の素性構造ライブラリを用いて、C++言語では記述しにくい「素性構造」や「単一化」を 多方面で活用できるようになっています。 LiLFeSの機能についてのより詳しい解説はこちらをご覧ください。

  • anarchy proof -

    Anarchy Proof This is a proof server. You can enjoy theorem proving here in several languages (one language). The list of all problems Create a new problems News return top

  • 圏論とラムダ計算の参考書 - (保存用) 檜山正幸のキマイラ飼育記 メモ編

    次のエントリー内で書籍に触れています。 groovyとラムダ式(6):補足と総括 - 檜山正幸のキマイラ飼育記 (はてなBlog)→プログラミング言語の基礎理論、プログラム意味論 ウルトラ・マクロな立場の定式化 - 檜山正幸のキマイラ飼育記 (はてなBlog)→プログラミング言語の基礎理論 見つけもの:Angelo Vistoliのていねいな論文 - 檜山正幸のキマイラ飼育記 (はてなBlog)→Categorical Logic and Type Theory, Handbook of Categorical Algebra 2 データ型のクレイジー計算 - 檜山正幸のキマイラ飼育記 (はてなBlog)→Categories and Computer Science 圏論、論理、計算論の関係については、"Introduction to Higher-Order Categorical L

    圏論とラムダ計算の参考書 - (保存用) 檜山正幸のキマイラ飼育記 メモ編
  • d.y.d. 文字コード&ベイズ推定

    12:21 06/05/28 うたひめ 先日の記事に書いたように KOKIA にハマりまして、 とりあえず片っ端から聴いてみることにしました。まずは 1st アルバムの 『songbird』 から … …4曲目の "白い雪" ヤバい。超ヤバい。なんだこれ。ツボすぎる。 ベスト盤を聴いたとき感じた揺らぎなく落ち着いた歌唱力的な曲を期待して聴きはじめたら、 予想外の声質の歌が飛び込んできてびっくりしました。もちろん抜群に巧いのに かわりはないんですが、ずっと儚げな、ガラス細工みたいなイメージの、ああ、その、 つまり白い雪みたいな雰囲気の綺麗な声で。その声と奇跡的にマッチしたメロディ。 すごいなあ。9曲目の "ありがとう…" もベスト盤でのリテイクと比べて同じ印象で、 Amazonのreview で TenderBerry さんという方が近いことを書いておられました。 しかし書いてて自分の語彙の

  • Mizar - Wikipedia

    自動証明検証システム Mizar(ミザー、ミザール)は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語(Mizar-言語)、実際にその言語で記述された証明の内容を検証することができる計算機プログラム(証明検証プログラム)、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ (MML) の三者から構成される。 Mizar と同様の目的を持つプロジェクトに、ロバート・ボイヤーのQEDプロジェクトがある。 システムの開発は1973年にアンジェイ・トリブレッツによって始められ、システムの保守をポーランドのビアリストーク大学(英語版)、カナダのアルバータ大学、日の信州大学で行っている。 Mizar-言語で記された証明文(以下、Mizar-論文)は普通のASCIIコードで書かれている。Mizar-言語は、数学の通常の言葉遣いと書式がよく

  • 1