bitterharvest’s diary
中学校の同期の仲間たちで、歴史散策と称して都内近郊の景勝地を定期的に訪れている。今回は、横浜の山手・山下地区にバラを見に行こうということになったので、その下見に出かけた。 この地域を、いかにも横浜らしいハイカラな街と感じている人も多いだろう。歴史的な建造物があちらこちらに立っていて、西洋館もある。なぜ、このような街並みができたのだろう。 この地域は、かつては居留地と呼ばれていたことを知っている人は少なくなった。子供のころ、お年寄りの人から、居留地と言われてキョトンとしたことを覚えている。そのころは外国の人を多く見かけるので、そのように呼ばれるのだろう程度にしか認識していなかった。 横浜市のデジタルアーカイブに明治23年の地図がある。中央左側の赤色の台形のところが山下居留地で、さらにその左側の同じく赤色で、裾が広がるようになっているところが山手居留地である。 なぜ居留地と呼ばれるようになった
Microsoft PowerPoint - ll2008.ppt
千年の言語？ A Thousand-Year Language? 住井 英二郎 Eijiro Sumii あんた誰？ Who am I? z いわゆるプログラミング言語「理論」の 研究者（大学准教授）です – ML（SML, OCaml）とかλ計算とか教えたり、 – いわゆる「型理論」とかプログラム等価性 とか研究しています – PerlとかRubyとか開発していません z すみません… � Academic researcher on programming language “theory” – Not developing Perl or Ruby (sorry...) 何でここにいるの？ Why am I here? z 趣味でMinCamlを作ったため（多分） – MinCamlって何？ ⇒ OCamlサブセットの教育用コンパイラ – OCamlって何？ ⇒ 関数型言語MLの方言
Project LambdaCan---Lambda Calculus in a Can
You can get soup in a can. You can get bread in a can (*). Now the long wait is over! You can finally get Lambda Calculus in a can. Project LambdaCan is an amusing exercise in absurdity. It implements a reducer (interpreter) for the Lambda Calculus, a formal system (programming language) developed by Alonzo Church in the 1930's to attack the deepest mathematical problem of the day. This was the En
de Bruijn indexについての備忘録 - rynaの紅茶日記
型システム入門で，de Bruijn indexの話で少しつまづいたのでメモ．型なしラムダ計算を前提とします． de Bruijn index de Bruijn index（ど・ぶらん・いんでっくす）とは，変数名として文字列ではなく，番号を振ってやることで表現を簡潔にしたものであり，ある場所に出現する変数が，どれほど外側で束縛されているかを表す数のこと． 言葉では分かりづらいので，次の図で． 青い矢印 対応する項 赤い矢印 束縛している場所 要点は， いくつ外側のλで束縛された変数かを意味するため，出現する場所により同じだった変数でもindexが変わる． 囲まれたλの個数以上のindexは，自由変数を表す． つまり，相対的な表記法である．（代入操作において重要） あと，型システム入門p.57に， この方法による実装が間違っている場合、微妙に失敗するのではなく壊滅的に失敗する傾向がある と
ド・ブラウン・インデックス - Wikipedia
ド・ブラウン・インデックス（英語: de Bruijn Index）とは、ラムダ計算において、名前を使わずに引数（束縛変数）を参照するための記法である。オランダ人数学者ニコラース・ホーヴァート・ド・ブラウンによって発明された。 解説[編集] この記法では、それぞれのλでは引数の名前を書かない。引数は、通常の記法でその引数を宣言するλが、何階層外側にあるかを表す自然数の番号で表記する。 例えば、λz. (λy. y (λx. x)) (λx. z x) は λ (λ 1 (λ 1)) (λ 2 1) となる。 ド・ブラウン・レベルは絶対的な位置を表すが、ド・ブラウン・インデックスは相対的な位置を表す。 参考文献[編集] De Bruijn, Nicolaas Govert (1972). “Lambda Calculus Notation with Nameless Dummies: A T
C++のテンプレートでラムダ計算と型推論 - 貳佰伍拾陸夜日記
C++のテンプレートを, コンパイル時に走るプログラムを記述するための言語だと思うと, この言語はチューリング完全なので, 当然ラムダ計算のインタプリタを実装できるし, そのラムダ計算の項の型を推論することもできる. できるからと言って馬鹿みたいにやってしまったという話. ソースコードは末尾. テンプレートメタプログラミング テンプレートをプログラミング言語だと思うと, 構文はともかく, 副作用がなく関数(っぽいもの)を淡々と定義してパターンマッチして再帰呼出しして, という感じでとても関数型っぽい. 関数と返り値 テンプレートメタプログラミングではテンプレートクラスを関数だと思って使う. そして返り値はtypedefして返す. たとえば任意の型S, Tを受け取って前者を返す関数firstは template<typename S, typename T> struct first { t
論理と計算のしくみ 5.3 型付きλ計算 (前半)
1. 輪講 — 論理と計算のしくみ 5.3 型付きλ計算 (前半) 伊奈 林太郎 (id:tarao) 京都大学 大学院情報学研究科 2012-01-26 伊奈 林太郎 (id:tarao) 輪講 — 論理と計算のしくみ 5.3 型付き λ 計算 (前半) 1 2. 参考文献 萩谷, 西崎. 論理と計算のしくみ. 岩波書店, 2007. J. C. Mitchell. Foundations for Programming Languages. MIT Press, 1996. B. C. Pierce. Types and Programming Languages. MIT Press, 2002. 伊奈 林太郎 (id:tarao) 輪講 — 論理と計算のしくみ 5.3 型付き λ 計算 (前半) 2
Lambda Calculus and Lambda Calculators
Beyond Church encoding: Boehm-Berarducci isomorphism of algebraic data types and polymorphic lambda-terms lambda to SKI: the first compositional translation Simplest poly-variadic fix-point combinators for mutual recursion Fix-point combinators are infinitely many and recursively-enumerable Many More Predecessors: A Representation Workout `switch' in lambda calculus Pairs, sums, etc. in System T/P
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
https://www.jstage.jst.go.jp/article/sugaku/66/1/66_0661078/_pdf
http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/sf07w/resume6.pdf
Curry-Howard同型から単純型付ラムダ計算の項を作る
https://www.cs.gunma-u.ac.jp/~hamana/Papers/typedlmd.pdf