サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
大谷翔平
fetburner.hatenablog.com
自宅サーバは一台あるだけで人生に彩りを与えてくれる素晴らしいものですが、帰省などで暫く家を留守にしていると、外出先からアクセスしたくなるもののインターネットに公開するのはセキュリティ的に怖い、といったジレンマが頭を擡げてきます。お正月の特番を眺めながら、これを録画サーバで撮れていればと何度思ったことでしょうか。 こんな時に丁度良いのがVPN接続で、通信内容を秘匿しながら自宅に居るかのようにネットワーク接続できるため、サーバをファイアウォールの外に晒す心配がありません。 本記事では、NECのVPN対応ルータであるIX2215を2個使って、自宅LANと実家LANとの間をVPNで接続したようなネットワークを構築します。これにより、セキュリティを担保しながら実家から自宅サーバにアクセスできるだけでなく、自宅に居ながらの実家ネットワーク保守も可能になる*1ことでしょう。 本記事で構築するネットワーク
この記事は言語実装 Advent Calendar 2020 の5日目の記事です. 一度でも型推論器を書いたことがあれば,そのあまりの邪悪さ,あるいはその複雑さに恐れ慄いたことでしょう. 参照を用いて単一化を実現しようものなら構文木は参照に汚染され,純粋関数型に実装しようものなら大量の型代入をどのような順序で適用したものか悩まされる. これは Hindley-Milner 型推論器を実装する上での宿命のようなものです. 本記事では,MLのサブセット——型付きλ計算をletと参照で拡張した,let多相をサポートする言語——の型推論器を Coq で実装し,その正当性を証明します. Coq で検証を行うことで我々は型推論器のバグへの恐怖とデバッグの労力から真に解放され,枕を高くして眠ることができることでしょう. もっとも、型付きλ計算を let 多相で拡張した言語の型推論器の正当性は実はすでに証
今年はそれらしきアドベントカレンダーが無いので,この記事は ML アドベントカレンダー 2020 の4日目の記事と言い張ってみます. ML って本を正せば定理証明支援系由来ですし.最後にちょっと OCaml を使ってますし. Coq によって検証された正規表現エンジンは既に存在していて,探せば他にもいくつもあると思うのですが, それらの実装は主として検証の簡単さに重きが置かれており,OCaml のコードを extract して使ってみると実用に堪えないものが多いように思います. 本記事では,以前 OCaml で書いた効率的な実装を Coq に移植して検証します. 加えて,extract によって OCaml のコードを再び生成し, AtCoder の問題に投げてみても TLE にならないことを確認します. 本記事で実装する正規表現エンジンと,その正当性の証明は GitHub に存在します.
これは型 Advent Calendar 2019 15日目の記事です. 交差型についてのよく知られた事実——交差型を持つ単純型付きλ計算において,強正規化する項は型付け可能であることを解説します. はじめに 交差型とは,読んで字のごとく型と型の共通部分を表す型です.すなわち,型を持つ項e(つまり )とは,型を持ち(),なおかつ型も持つ項()を指します.交差型のある体系では,SMLの+のようなアドホックな多相性1をのように表現できる嬉しさが知られています.しかし,真にヤバい点と言えば後述する性質でしょう. 交差型を含むある種の言語——交差型を持つ単純型付きλ計算——において,任意の項の型付け可能性と強正規化性は一致することが知られています.確かに左の性質から右の性質は導けそうです.単純型付きλ計算,System F,CoC等々,多くの言語において,型付けできる項は強正規化する2ことが知られ
僕の所属する研究室では毎年Software Foundationsの輪講をやっているんですが,Brzozowski derivativeに基づいて正規表現エンジンを実装し,あまつさえCoqで検証してしまおうといった練習問題が追加されていて大変興味深かったです. 折角practicalなプログラムを書いたのにCoqの中に閉じ込めておくのも勿体ないですし, OCamlで同様の正規表現エンジンを実装し,実行速度を見てみようと思います. *1 2018/12/16 Brzozowski derivativeの定義に誤りがあったため修正 Brzozowski derivativeとは? ある正規表現が受理する言語の先頭から,文字を取り除いて得られる言語 *2を受理する正規表現をBrzozowski derivativeといい,以下のようにsystematicに求められます. ある正規表現が空文字列を
この記事はML Advent Calendar 2017の10日目(!?)のために書かれました. 皆さんOCaml標準ライブラリのList.sortは使っていますか? 頻繁にリストに対してのソートを行うようならデータ構造かアルゴリズムを考え直した方が良いでしょうが,競プロの様にちょっとしたプログラムを書く時には僕もよくお世話になります. マニュアルによると,そのList.sortはマージソートで実装されているようですが,僕のような者がちょっとやそっと工夫した程度では敵わないような最適化が施されています.今回はそのソースコードを読んでみましょう. まず,OCaml 4.06.0のlist.mlから引っぱってきたList.sortのソースコードを見ていきましょう. (** sorting *) let rec merge cmp l1 l2 = match l1, l2 with | [],
この記事は言語実装 Advent Calendar 2017の10日目(!?)のために書かれました. 9日目の記事は@ukitakaさんのSwiftコンパイラで採用されているパターンマッチの網羅性チェックの理論と実装です. 何やら言語実装Advent Calendar 2017に型推論器の実装をやろうとしている人がちらほら居たので,先にlet多相の型推論の実装と形式的検証をやって威嚇しようと思ったのですが,論文とワークショップで死んでて遅刻してしまいました…お恥ずかしい… まだ単純型付きλ計算にしか対応していませんが,「Done is better than perfect.」ってことでこのまま記事にしてしまいます. let多相に対応できたらまた別のAdvent Calendarに投稿しましょう. 今回書いたコードはGitHub上で公開しています.https://github.com/fe
この記事は言語実装 Advent Calendar 2016の9日目ために書かれました。 最近僕はcall-by-needに関連する研究をしており、気分を理解するためにcall-by-needを採用した言語のインタプリタをStandard MLで実装したりしました。今回はその時の事でも記事にしておきましょう。 Call-by-needとは? Call-by-needとは、評価戦略の一種です。評価戦略と言えばcall-by-valueとcall-by-nameが有名でしょう。 Call-by-valueは最も右側のredexから簡約する評価戦略で、例えば(λx. x x) ((λx. x) (λx. x))は (λx. x x) ((λx. x) (λx. x)) → (λx. x x) (λx. x) → (λx. x) (λx. x) → λx. x と簡約されます。ちなみにλの中は簡約
この記事はTheorem Prover Advent Calendar 2016の4日目のために書かれました。 少し季節外れの記事になりますが、前期はプロ演A^1の季節でしたね。 僕のTLでもC言語の課題に苦しめられた学部生のツイートが良く回ってきましたが、 とりわけ彼らが苦戦していたのはマージソートを書く課題のようでした。 面白そうなので僕もCoqで実装してみましょう。 もちろん、証明付きで。 実装 とりあえず比較関数等の準備 Require Import Arith Div2 List Orders Sorted Permutation Program. Require Omega. Section MergeSort. Local Coercion is_true : bool >-> Sortclass. Local Hint Constructors Permutation St
最近研究でCoqぐらいしか書いてないので、リハビリがてらAtCoderで 開かれるコンテストにOCamlで参加して遊んでます。 僕は個人的な趣味もあってOCamlを使う際は専ら言語処理系を書いていましたが、 競技プログラミングでは全く関係ない題材を扱う必要があるので新鮮な感じですね。 それに伴って有名なアルゴリズムもいくつか実装したので、 ここではそういうアルゴリズムをMLではどう書いたのか紹介したいなと思います。 高速なべき乗のアルゴリズム 正式名称はよく分からないのですが、ありますよね?O(log n)でべき乗を計算するアルゴリズム。 x ^ nを計算する時、nが偶数の時は(x * x) ^ (n / 2)とみなすやつです。 OCamlで素朴に実装するとこんな感じ。 let rec power m = function | 0 -> 1. | n when n mod 2 = 0 ->
このエントリはML Advent Calendar 2015と言語実装 Advent Calendar 2015の20日目の記事です。 言語実装 Advent Calendar 2015の19日目の記事はh_sakuraiさんのJavaのサブセットコンパイラの作成でした。 タイトルの通り、Standard MLでコンパイラを書いた話をします。 対象言語はSMLのサブセットで、仮想機械の命令を出力します。 対象言語 だいたいこんな感じ SMLを触った事があれば何となく分かりますよね…? SMLのサブセットと言いつつ、λ計算にintとboolとタプルとletを入れて中置演算子のサポートを手厚くしたような感じです。 +, -, *, <=の四つの中置演算子が予め定義されています。 仮想機械 無限個のレジスタがあって、レジスタの内容が指しているアドレスにジャンプできるような仮想機械です。命令セット
このエントリはTheorem Prover Advent Calendar 2015と言語実装 Advent Calendar 2015の11日目の記事です。 言語実装 Advent Calendar 2015の10日目の記事はkeenさんのリージョンについてでした。 最近ではC++等にまで実装されているので皆さん型推論が何かは想像が付くでしょうが、どのようにして実装されているかは知らない方も居るかもしれません。 例えば、1+2*3のような関数を含まないtermに型を付けるのは簡単ですよね。 subtermの型を見てボトムアップに型を付けていけば良いだけです。 (* 関数抽象を含まないtermに対する型付けのイメージ *) (* 型付けに失敗した時に投げる例外 *) exception IllTyped (* 型 *) type typ = | Int | Bool (* term *)
この記事はML Advent Calendar8日目の記事として書かれました。 7日目の記事はでこれきさんのfoldみぎひだりです。 Standard MLやOCamlをはじめとしたML系の言語は関数型言語として有名ですが、参照、配列、例外といった副作用を伴う機能も扱う事ができます。 また、ML系の言語で手続き的に書いたからと言ってその言語の魅力が損なわれるわけではなく、 強い静的型付け、型推論やparametric polymorphismなどの恩恵を受けられるので、むしろ良く設計された手続き型言語のように映る事でしょう。 積極的にMLで手続き的な処理を書いていこうな。 2015年12月8日1:05 Kleene's algorithmの実装を間違えていたので修正 2015年12月8日17:54 プログラムの例をリファクタリングした 手続き的な処理と言えば僕はグラフ関連のアルゴリズムが思
このページを最初にブックマークしてみませんか?
『fetburner.core』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く