名残

プレゼント・デイ プレゼント・タイム

日記 (2021/06/24)

今日は仕事が休みだった母と一緒に買い物に行ったり、今日サービスが開始されたばかりのスマホゲーム「IDOLY PRIDE」をプレイしたり、「生の短さについて」の続きを読んだりして過ごした。

IDOLY PRIDE をプレイしはじめた

IDOLY PRIDE はアイドル育成ゲームで、地道にアイドルの各パラメータを伸ばしてライブの曲にあわせて編成を調整したりする。ひとつひとつのライブの成功やアイドルグループ全体の順位の向上が目標になっている。ゲームシステムが細かな部分まで丁寧に作り込まれていて、担当アイドルとの不定期のコミュニケーションなどもあるので、プロデューサーとして彼女たちを育てて上げたいという気持ちにさせてくれる。かなり愛着のわく作業ゲームだなぁと思った。一時期デレステにハマっていたが、久しぶりのスマホゲームとしてこれにどっぷりハマるかもしれない。

「生の短さについて」要約

第7章 後半

しかし自分の生の多くの時間を奪い取られる者が、生が不足していると自覚するのは当然のことではないか? 君を招きよせ忙殺させている者は皆、いわば君を君自身から拐かしている。 自分のために残せた時間はごくわずかで使いものにならない。 誰もが今の地位・仕事に倦怠感を覚えて、生を先へ先へと急がせ、未来への憧れにあくせくする。 それに対して、一日一日を最後の日であるように管理する者は、明日を待ち望むことも恐れることもない。 彼らにとって、未来は大体が既知のものであり、それ以外は時の運に決めさせればよくて、その生には付加できるものはあっても取り去れるものはない。 それゆえに、見かけ上は老いているようでも、それは長くいただけのことであって、長生きしたとは言えない場合がある。

第8章

物に比べて時間は軽々しく要求・貸与されがちである。 時間は何よりも貴重なものであるのにそんな考え違いをしてしまうのは、時間に形がなくてほとんど無価値なものに思えてしまうからだ。 湯水のように時間を使っておいて、 死が近づくと急に命が惜しくなるという情緒は首尾一貫していない。 自分の生に残された時間がわからないからこそ、時間は注意深く大切に扱わなければならない。 もちろん時間の大切さを一切理解していないというわけではないだろう。 愛している人に対して「自分の時間を捧げる」と言うものだが、 捧げものとはいえ、自分の時間は減っても相手の時間は増えない。 このことを自覚できていないのである。 人の生は出発点となった日から一直線に駆け行く。 そのため、君が何かに忙殺されていればそのうち死が訪れ、その死とともに永久に安らわなければならなくなる。

第9章

人は生を犠牲にして生を築こうとする。 あれこれ未来について思いを馳せる。 これこそ最大の浪費であり、 明日という時に依存して今日という時を無にする。 どこを目指しているのか? 不確実な先々の事を気にするのはやめ、ただちに生きるべきだ。 何かに忙殺されるような稚拙な精神だと、何の備えもないまま老年に襲われる。 矢のように過ぎ行く生の時間の終着点は、 こういう者の前には最後になって急に現れる。

第10章も読んだが時間がないので明日の日記で要約を載せることにする。

日記 (2021/06/23)

ゲーセンと本屋に行った。 ゲーセンでは CHUNITHM をプレイし、本屋では「人間の学としての倫理学 (著: 和辻哲郎)」と「コンビ二人間 (著: 村田 沙耶香)」購入した。

f:id:u0918_nobita:20210623153711j:plain

f:id:u0918_nobita:20210623155101j:plain

帰宅後はプログラミングのお仕事をした。 それが済むと APEX をした。友人とボイスチャットをつないで一緒にランクマッチをプレイするのが楽しかった。最終的にはシルバー2に上がった。

「生の短さについて」要約

第7章 前半

生の時間を浪費する人間に着目すると、口腹の欲と性欲のために生の時間を浪費している人間は特に醜く、何かに忙殺される人間は何事も立派に遂行できないことがわかる。いろいろな事に関心を奪われて、何事も深く心に響かないからだ。そういう人間の属性として、真に生きることの自覚が薄い。生きる術はほかの技芸とは異なり、生涯をかけて学ぶべきことであり、死ぬ術も生涯をかけて学ばなければならない。

多くの偉人たちは、生きる術を学ぶのに全生涯をかけていた。しかも彼らのなかには、自分はそれを今だに知らないと告げて亡くなった人も多い。人間的な過誤を超越した偉人は、自分の時間が奪われることを許さない。彼らは自分の時間と交換できる価値あるものを何も見出せなかったのである。彼らにとっては生は十分に長かったのだろう。

日記 (2021/06/22)

お昼に起床し、「生の短さについて」の続きを読んだ。

  • (第6章) リーウィウス・ドルーススは精力的な活動家だったが、子供の頃から裁判で特異な影響力を行使していて、全く落ち着くことのない自分の生を呪っていた。彼の早熟な野心は猛進し、結局公私ともに不幸になった。彼のように「他人には至福の人と思われていたが、本人は自分のこれまでの行動を悉く憎悪し自らを弾劾した人たち」は、その嘆きでは他人も自分も変えることができなかった。本音を漏らしたところで、また同じような状態に情緒が戻っていくからである。君たちの生は、たとえどんなに長く続こうと、必ずやきわめて短い時間に短縮されるだろう。なぜなら、これまで挙げたような悪習が悉く時間を喰らい尽くすからだ。「時」は万物のなかで最も足早に過ぎ去るものであり、理性を用いれば歩みを遅くすることはできるが、放置すれば君たちから逃げ去るのは必然である。
  • (第7章も読んだが要約を推敲しているうちに午前4時を過ぎてしまったので、明日の投稿に第7章の要約を含めることにする)

16時ごろにサイクリングに出かけて、帰りがけに「小説 機動戦士ガンダム 閃光のハサウェイ」の中・下巻とVTuber チップス第3弾8袋を購入した。帰宅してすぐ風呂に入ってサッパリしたらVTuberチップス開封の儀を執り行った。お目当ての「小森めと」カードが1枚当たってテンションが上がった。ただシンプルな紙製のカード1枚がついたポテトチップス1袋が税込み242円は高すぎやしないか?とも感じた。

夕食後、深夜までぶっ通しで APEX をやってしまった。ランクマッチでポイントを貯めてはやく次のティアにランクアップしたいと思っているが実際にやってみるとポイントの増減が激しく、ついつい長時間やってしまう。

日記 (2021/06/21)

お昼に起きて、夕方にロードバイクに乗って近所のコンビニまで行った。欲しかった VTuber チップス第3弾(今日発売だったやつ)は見つけられず、結局 LINE PAY の残高を追加する手続きだけして帰った。ド田舎のコンビニは数日遅れて新商品が並ぶのでそもそもあまり期待はしていなかった。明日も天気が良ければ運動がてらコンビニに行こうと思う。

夜には PC を開き、Auth0 という認可認証の SaaS に初めて触れてみた。ほんの数十分でSPAでのログイン機能を実装できて拍子抜けした。OpenID Connect あたりの技術を、実際に手を動かしながら学ぶ必要性を感じた。

日付が変わる少し前には「生の短さについて」の続きを読み始めた。ここにきちんとまとめる気になれなかったのは、今日読んだ部分が正直面白くなかったからだ。とにかく似たような例示が多くてさすがにくどいと感じて斜め読みした。目標を示さずに初っ端から具体例ばかり長々と書いてしまうと読者の関心を著しく失うという教訓にはなった。今日読んだ部分の内容をすごく雑にまとめると以下のようになる。

  • (第3章) 生を浪費してしまうのは、いずれ死ぬものであるかのように全てを恐れて、不死であるかのようにすべてを望み、若いうちにしかできないような事を老後に先延ばしするからだ。死すべき身であることを失念しているのは愚かだ。
  • (第4,5章) アウグストゥスキケローのような高い地位の人々は、そろって「閑暇」を称え切望していた。それは、栄えた者は誰にも影響されなくともいずれ自壊することをわかっていたためで、時としてその頂きから降りたいとも願っていた。この2人は終身歴史に翻弄され、ついに閑暇を得ることは出来なかった。生前は閑暇を夢見たり逆境に耐える自らを賞賛することで労苦を癒していた。閑暇こそが、万人の願望を叶えられた人の切なる願望であった。

生を浪費することの愚かさについて長いこと説教をした後で急に暇について話始めたのには、どんな意図があるんだろうか?先に挙げた「貧欲や怠惰で生を浪費する人々」の対極として「人の上に立ち力を尽くしていたが自らの平安は得られなかった人々」を挙げたのだろうか?そこらへんの繋がりや結びが少し気になってきたところで、今日はもう眠いので文字を打つのをやめて投稿ボタンを押す。

ピクシブの就業インターンに参加しました

9/4~13でピクシブインターン2019に参加しました。

recruit.pixiv.net

TL;DR

  • pixivFACTORY をチーム開発する一体感を感じられた
  • 初めて複雑GUIに触れた
  • React Hooks / SVG はいいぞ

選考・参加の動機

自分の GitHub アカウントを紹介して、そこにある成果物とオンライン面接で選考を受ける「GitHub 選考」でエントリーしました。 様々なコースがありましたが、中でも自分が使ったことのあるサービスで、かつ仕組みが面白そうな pixivFACTORY のコースを選びました。 pixivFACTORY は、少なくとも画像1つから様々なグッズをデザインしてそのまま購入できるサービスです。 就業型インターンということで、オフィスの雰囲気や働き方、チーム開発などについて実践を通して深く学ぼうと考えて参加しました。

github.com

factory.pixiv.net

やったこと

Webフロントエンドを担当し、グッズのデザインを編集する画面(以下、エディタ)のリファクタリングとプロトタイプの作成をしました。TypeScript, React, Redux (+ Thunk), DOM とひたすら格闘する日々でした。主に f_subal さんにメンターを担当していただいていました。

技術面

初めての React Hooks

関数コンポーネントの定義のなかで特定の組み込み関数を使って、 ステート・componentDidMount/Updateでの非同期処理・ref などの機能を利用できる機能です。 既存の複雑なクラスコンポーネントリファクタリングしていく上で強力な機能だということを実感しました。

ja.reactjs.org

(ステートフック、これ使ったら実質クロージャやんけ…すき)

初めての Redux Thunk

今まで Redux Saga を使ってジェネレータ関数で Side Effect を実装していました。 Redux Thunk は、非同期処理をそのままアクションとして投げると実行してくれるという機能のみを提供する Redux ミドルウェアです。 実際に使ってみると「正直 Saga のような複雑な仕組みを用いなくても Thunk だけで十分なシチュエーションは多いな」という感想を持ちました。

github.com

これが複雑GUI

エディタで画像やテキストを追加してある場合にそれぞれ表示されるバウンディングボックスを SVG で実装しているコードを読んで衝撃を受けました。そこから複雑GUIに関して、いろいろな技法を会得しました。 例えばドラッグ操作に関して、「イベントハンドリングを確実に行ってスムーズにSVG要素の座標を更新するために、ドラッグ中であることを検知するためのイベントハンドラを document 要素に追加してしまう」という大技も知ることができました。(f_subal さんによると、これは常套手段らしいです)

SVG すごい

もともと存在は知っていましたが、viewbox の機能も知らないレベルでした。 f_subal さんの SVG 芸を知って、自分もこれからフロントエンドのベクターグラフィックスにガッツリ触れていきたいと思うきっかけになりました。

感想

この短期間で、フロントエンドの技術はもちろん、チームで進捗を管理しながらサービスの開発と運営を行う現場の雰囲気や開発の流れについて深く知ることができました。また、社内勉強会等を通じて、異なるチームに属するエンジニア同士でも積極的に楽しく技術を学んでいける文化に触れることもできました。この貴重な経験を、今後のエンジニアとしての人生に存分に活かしていきたいと思います。

言語処理系周りの用語とコンパイラの構造

これからは、自分が興味を持った技術とか理論に関して書き散らしていくつもり。
おそらく当面は ↓ の本を読んだ感想とか言語処理系の開発進捗について載せていく

今日は「コンパイラの構成と最適化」を読み進めたので、その要約を書く


1章「はじめに」

言語処理系周辺の用語の定義

1. コンパイラ

高級言語で書かれたプログラムを、機械向き言語 (計算機での実行に適した言語) のプログラムに翻訳するためのプログラム

2. 変換系

ある言語 (原始言語) で書かれた (原始) プログラムを他の言語 (目的言語) の (目的) プログラムに変換するためのプログラム

3. インタプリタ (翻訳系)

高級言語に都合よく設計された VM の言語 (中間言語) に変換して、それを解釈実行するプログラム

計算機が特定のプログラム言語に対して設計されているわけではなく、高級言語で書かれたプログラムを機械語のプログラムに直接変換するのは難しいことが多いため、よく用いられる

利点:コンパイラ / インタプリタの開発が比較的容易

欠点:目的プログラムの実行速度が遅い

4. 前処理系

原始プログラムのレベルで前処理的な変換を行う変換系

5. (言語)処理系

原始プログラムのコンパイルから実行までに必要なすべてのシステムを合わせたもの

関係性の図式化

↓ こんな感じ

2章「コンパイラの簡単な例」

コンパイラの論理的構造/物理的構造について説明されていた。
式の構文解析を理解するための準備としてスタックの原理と後置記法、操車場アルゴリズムが解説されていたがググればすぐわかるので言及しない。

コンパイラの論理的構造

1. 字句解析

(入力: 原始プログラムの文字列, 出力: 解析結果を表すトークン列)

原始プログラムのソースコードを先頭から1字1字調べながら、プログラムの基本要素であるトークンを切り出していく

2. 構文解析

(入力: トークン列, 出力: AST (抽象構文木))

プログラムのどの部分がどの文法規則に対応するかを解析し、文法的に正しければその構造を反映した木構造データである AST を出力する

3. 中間語生成

(入力: AST, 出力: 中間語)

AST をそのまま中間語とすることもあるが、より目的コードに近い形として AST の構成要素を実行順に整列したものを中間語とすることもある。複数の中間語を用いるコンパイラもある

中間語の例:RTL (Register Transfer Language)
レジスタとのデータのやり取りを手続き的に記述する中間表現 (intermediate representation) で、GCC でも実際に使われているらしい。すごい

※ これを構文解析と同時に行うコンパイラも存在している

4. 最適化

(入出力: 中間語)

目的プログラムを、実行効率のよいものにする

中間語の列の中で無駄なものを省いたり、順序を入れ替えたりして、より効率のいい目的プログラムを吐き出せるようにする

最適化のタイミングは様々:

  • 構文解析の直後
  • 中間語の生成直後
  • 目的コードへの変換直後

5. コード生成

(入力: 中間語, 出力: 目的プログラム)

機械語の目的プログラムを生成し、ファイルに出力する

主ルーチンからサブルーチンまで、そのプログラムの実行に必要なプログラムをまとめて一度にコンパイルする場合は、コード生成完了後にすぐ実行することができる

C や Fortran などのように、主ルーチンやサブルーチンを別々にコンパイルする場合は、目的プログラムは別々のファイルに出力される。それらを結合して実行可能ファイルを出力するには、リンカやリンケージエディタが必要になる

コンパイラの物理的構造

相 (Phase)

コンパイラの論理的構造の各段階を指す

パス (Pass)

言語処理系のなかで、1つの言語の変換を担当するルーチン群

例えば字句解析と構文解析が異なるルーチンに分離され、ソース全体をトークン列に変換したものを字句解析ルーチンから構文解析ルーチンに渡す構成の場合、ここには2つのパスが存在していることになる

構文解析ルーチンが先行して呼び出され、サブルーチンとして適宜字句解析ルーチンが呼び出される構成の場合、1つのパスにまとまっていることになる

パスコンパイラ

論理的構造のすべてを1パスにまとめてしまう実装

中心的役割を担うのは構文解析ルーチンで、通常は最適化の相がない

コンパイル時間が短いのでデバッグ時には都合がいい

マルチパスコンパイラ

複数のパスに分かれた実装

複数の原始言語に対応するには「字句解析」〜「中間語生成」のパス (フロントエンド) を原始言語ごとに開発して、以降のパス (バックエンド) は共通化すればいい

さらに複数の目的言語に対応するには「コード生成」のパスだけを目的言語ごとに開発すればいい (この場合「コード生成」のみがバックエンドに属する)

特に最適化のためのパスを持ったものを「最適化コンパイラ」と呼ぶ

最適化の効果を高めるためには各種の解析が必要になるので、そのためにパスをさらに複数に分割することも多い

なお中間言語を実際のマシンに依存しない形にすれば、その最適化のパスは共通化できる

複数のパスに分ける他の理由

  • メモリの節約 (昔のコンパイラはメモリ不足になるのを防ぐためにパスを分けてたらしい)
  • 言語仕様 (例えば飛越し命令を含む目的プログラムを吐き出すのが厄介だったりするらしい)

雑なまとめ

今回はまぁ言語処理系・コンパイラに関しての基本的な概念を整理する感じだったので「それはそう、大事」って感想しかない

これからは具体的な字句解析・構文解析の理論や実装に触れていく予定

あと今まさに開発している、自作言語「Psyche (プシュケ)」を wasm に変換するコンパイラについての話も絡めながら進めて行けたらいいなぁ、なんて考えている

おしまい

操作的意味論とか数理論理学とか Coq とか

TL;DR

  • いろんな本を使って操作的意味論と数理論理学を学び始めた
  • MBP にインスコした CoqIde で Coq を書き始めた
  • #100DaysOfCS を始めた

はじめに

先日、大学の図書館でいろいろと本を借りてきました。

操作的意味論や数理論理学を学んで、プログラミング言語についての理解を深めることが目的です。
今回は上で太文字にしてある2冊を扱いますが、他の本についても、また別の記事で言及したいと思います。

操作的意味論について

CoPL を使って学んでいます。操作的意味論は、プログラムをどのように操作・計算して実行結果を得るか、という視点からの「意味の与え方の体系」です。プログラムの意味論はこれを含めて3種類あり、あとの2つは「公理的意味論」と「表示的意味論」です。「プログラム意味論」という本で詳しく解説されているらしいので、後々学んでいきたいと思います。

CoPL には優れた「演習システム」があり、Webサイト上で演習問題を解いて、自動採点機能を利用することができます。今は算術式の評価・簡約に関する演習問題を解き進めています。今後メタ定理の証明を行うので、後述する Coq で記述してみようかなぁと思ってます。

数理論理学について

情報科学における論理」という本を使っています。
今は第1章「命題論理」で充足可能性について学んでいます。

CoPL で今後学ぶ「推論」などの分野で、この数理論理学で学んだことが役に立つらしいです。

Coq に入門した

ここまで紹介してきた2冊には、証明問題がいくつも掲載されています。
もちろん僕も手を動かしてそれを解いてますが、PC上で専用の言語を使って半ば機械的に証明をしたり、証明の過程をテキストに起こして GitHub 等で管理したいという思いがありました。

このような理由から、前々から気になっていた Coq に触れてみることにしました。
Coq はプログラムの仕様を検証するためによく用いられる証明支援システムです。
今の僕にはよく分かりませんが、高階述語論理というものを採用しているため、検証器としての表現力はかなり高いらしいです。

環境構築

MacBook Pro (2017) に導入することを想定しています。
まず、GitHub リポジトリの Releases ページから dmg ファイルを落とします。
今回は Pre-release ではなく Latest release の 8.8.2 をダウンロードしました。
マウントすると .app ファイルが入っているので、Applications フォルダに移動して起動します。

さっそく定理証明してみる

手始めに、f(x) = x + 100, g(x) = x - 100 を定義して、定理 g(f(x)) = x が成り立つことを証明します。 エンジニアHubというサイトのこの記事を参考にしました。見よう見まねで証明を記述してみます。

帰納法を使って証明してみる

こんな風に、induction タクティクスで帰納法を使うことができます。
フォロワーさん曰く、fix タクティクスや inversion タクティクスを用いることも出来るらしいです。

※ タクティクス:Coq の証明開発モードで用いる道具

まとめ・目標

初のブログ記事ですが、いかかでしたか?

実は昨日から、100DaysOfCS (CS=Computer Science) ということで、100日間CS関連の理論を学んで、毎日進捗を報告し続けるチャレンジを始めています。

ある程度進捗が出たら、まとめてこのようなブログ記事にして公開するので、これからもよろしくお願いします!