「プログラミング・シンポジウム」へ戻る

日程

2020年1月10日(金) 12:30 受付開始

2020年1月10日(金) 13:30 開会

2020年1月12日(日) 12:10 閉会

会場

ラフォーレ倶楽部伊東温泉湯の庭

 

（新たな試みとして、各発表の概要の掲載をテストしています。「概要」をクリック・タップすると概要の表示がOn/Offされます。）

第1日 1月10日

開会，ガイダンス 13:30 - 13:40

セッション1（教育） 13:40 - 15:00 座長：和田 勉（長野大学）

プログラミング言語ビスケットを学び続けた児童のプログラムの分析

渡辺勇士 (合同会社デジタルポケット, 電気通信大学), 中山佑梨子, 原田康徳, 久野靖

概要

本発表では，幼稚園からビスケットを使ってプログラミングを学んでいる，児童の作ったプログラムについて報告する．我々は，幼稚園年長からビスケットを学び続けている，小学校2年生から4年生がプログラミングコンテストに応募するために作成した作品を収集した．そして，それらの作品の中で何を，どのように，どうやって，児童がプログラムでコンピュータ上に表現しているかを分析した．分析は，児童が作った作品自体と，児童自身による作品の説明とで行なった．その結果，園児一人一人によって，多様な作品が作られており，また，全ての児童が自分の作ったプログラムを説明できることがわかった．

発表資料

3人の賢者の復讐

竹内郁雄 (東大名誉教授)

概要

2016年のプログラミングシンポジウムで発表した「3人の賢者の問題」とそれを解くプログラムには致命的な論理誤りと，他の賢者の思考を推論するプログラミング手法の選択ミスがあった．ここではその誤りを正すとともに，新しく分かった興味深い数理的事実と，実際のゲームのシミュレーションプログラムについて述べる．

発表資料

セッション2（定理証明） 15:20 - 16:40 座長：中野 圭介（東北大学）

項書換による証明付き最適化

池渕未来 (マサチューセッツ工科大学)

概要

プログラムの最適化には，たとえばshort cut fusionのように項書換として実現できるものが多くある．書換による最適化が実用されている例として，HaskellのコンパイラであるGHCは，Haskellプログラムに対してプログラマの指定した書換規則を適用し最適化する機能を持つ．一方，証明支援系Coqは自動証明機能の一環として，等式証明のための自動的な書換の機能を持っている．今回の発表では，その機能を利用してCoqで記述されたプログラムを最適化する方法について示す．この方法ではプログラムは最適化されるだけではなく，最適化前のプログラムと最適化後のプログラムが同じ振舞いをすることが自動的に証明され，最適化の安全性が保証される．具体例として，リストを操作する関数に対する簡単な書換規則による最適化や，さらに高速フーリエ変換の一般的な場合に対する実装から特別な場合での効率的な実装の導出を見る．

Agda 上でのZF集合論の構成

河野真治 (琉球大学工学部)

概要

Agda は省略可能な型変数を持つ純関数型言語であり、カーリーハワード対応に基づく証明支援系として使うことができる。数学的な命題は型として記述され、その証明は型を実現するλ項として記述される。ここでは直観主義論理に適した非構成的な仮定を導入し、ZFC集合論の公理を証明する。集合はデータ構造である順序数上の述語(Ordinal definable)として導入する。

発表資料

ポスターセッション紹介，各種報告，スポンサー講演 ( 株式会社インターネットイニシアティブ ) 17:10 - 18:00

スポンサー講演資料（株式会社インターネットイニシアティブ）

夕食 18:00 -

ポスター・デモセッション，GPCC 19:30 - 21:00

<ポスター・デモ> オンラインプログラミング環境Google ColaboratoryにおけるPythonの導入実践例

山本周，清水克彦 (東京理科大学大学院)

<ポスター・デモ> 項書換による証明付き最適化

池渕未来 (マサチューセッツ工科大学)

<ポスター・デモ>継続を基本としたOS Gears OS

清水隆博, 河野真治 (琉球大学)

概要

継続を基本とするCと互換性のある言語、 Conitinuation Based C(CbC)を用いてOSの実装を考案した。状態遷移単位でOSの処理を実装することで、 処理の入出力が明確化され、 定理証明支援系に適した表現形式で処理が記述可能である。CbCを用いて開発しているOS、 GearsOSはXv6をベースに実機での動作を目指している。現在までにGearsOSはCMakeを利用することで、 マルチプラットフォーム上でクロスコンパイルすることが可能となった。

<デモ> プログラミング入門教育における短冊型問題の活用

久野靖 (電気通信大学)

<デモ> 自由文思考プログラミング環境における手続的機能の実装

中村圭介 (ナレルシステム株式会社)

<デモ> プログラミング言語ビスケットを学び続けた児童のプログラムの分析

渡辺勇士(合同会社デジタルポケット,電気通信大学),中山佑梨子,原田康徳,久野靖

<デモ> Elixir におけるC言語コード生成・最適化の試み

山崎進 (北九州市立大学), 久江雄喜

<デモ> FPGA/GPU/CPUが集積されたヘテロSoC環境におけるプログラミング

佐藤健太,佐藤幸紀 (豊橋技術科学大学)

第2日 1月11日

セッション3（正規表現） 9:00 - 10:20 座長：新屋 良磨（秋田大学）

静的型つき組版処理システムSATySFi

諏訪敬之

概要

本稿では，2017年度未踏事業の1プロジェクトとして著者が開発し，現在も発展を続けている新しい組版処理システムSATySFi（サティスファイ）について紹介する．このシステムは（TeX/LaTeXと同様に）或る種のマークアップ言語とその処理系として実装されており，ユーザやパッケージ開発者が独自にコマンドを定義して使用することも可能である．従来システムとの顕著な違いのひとつは，OCamlによく似たいわゆる函数型言語を使用してコマンドを平易に定義できることにある．また，函数型言語を採用した恩恵として型検査器が搭載されており，或る種の不適格な入力を与えた際に素早くわかりやすいエラーを静的に（＝実際に組版処理が行われるよりも前に）提示してくれるため，従来システムに比べて高い執筆効率が期待される．本文では，SATySFiに於いて型の観点から組版処理をどのように定式化したかや，最近追加しつつある多段階計算に基づくマクロ機構の紹介など，特に計算機科学の知見が援用されている点について述べる．なお，本稿もSATySFi製である．

発表資料

Ken Thompsonの正規表現探索アルゴリズムを解剖する

和田英一 (IIJ技術研究所)

概要

Ken Thompsonの正規表現探索アルゴリズムは正規表現をIBM 7094の機械語に変換するAlgol 60で記述されたコンパイラと, IBM 7094のアセンブリ言語で記述された実行時に使うサブルーチン類で説明されている. つまり探索を機械語のプログラムで直接実行し, 速度を稼ごうという発想である. 実行時処理では,サブルーチンと, コンパイラの生成した機械語プログラムと, これらのプログラムが実行中に生成する機械語プログラムが入り乱れて走り, 解読が難しい.本稿ではThompsonプログラムの仕組みと, プログラムで作ったプログラムが走るvon Neumann型アーキテクチャを活用した時代のプログラムの面白さを説明する.

発表資料

セッション4（処理系） 10:40 - 12:00 座長：水島 宏太（株式会社オプト）

FPGA/GPU/CPUが集積されたヘテロSoC環境におけるプログラミング

佐藤健太,佐藤幸紀 (豊橋技術科学大学)

概要

FPGAやGPUをアプリケーションに特化する形で活用することは，処理速度と低消費電力性の両面から有望なアプローチとして注目されている．しかしながら，それらのデバイスをどのようにプログラムするかについて，多くの事例が紹介されているとは言えない．本稿では，FPGA/GPU/CPUを搭載したSoCの開発ボードであるUltra96を用いて，Julia集合を高速に描画し，接続したゲームパッドを用いてインタラクティブに操作可能なシステムの事例を紹介する．フルスタックでシステムを動作させるために必要となったプログラミング環境やプログラミング技術についての概要を述べ，特に，高位合成技術を活用してハードウェア記述をソフトウェアとして抽象化した実装と，同等のシステムをハードウェア記述言語 (HDL) を用いて実装した場合について，生産性や性能面で比較を行う．加えて，ハードウェアとソフトウェアの垣根を超えるプログラミング技術に関しての考察を行う．

発表資料

Elixir におけるC言語コード生成・最適化の試み

山崎進 (北九州市立大学), 久江雄喜

概要

我々は Pelemay Super-Parallelism と称する関数型言語ElixirからC言語へのコード生成・最適化を行う処理系を研究開発している．これは，ElixirにはElixirのコードをASTに変換する機構が備わることを利用し，並列化可能なコードを検出してC言語コードを生成し，Auto Vectorization を利用してSIMD並列化を行う処理系である．2019年10月に公開したバージョン0.0.4では，あらかじめテンプレートとして定義されたC言語コードにコードを埋め込む方式のコード生成を実装し，元のElixirコードと比べて約2倍の高速化が図れた．2019年11月現在研究開発中のバージョン0.1.0系列では，コード生成の方式を大幅に見直し，柔軟なコード生成を図れるようにする予定である．本発表では，その中で最も特徴的な型検査の最適化方法について提案する．これは，動的型言語であるElixirの型の特性と，NIFという Elixir とネイティブコードの間のFFIを利用して，型検査と型推論を並行して実行することで，型検査の最適化を図る方式である．今後，実装と性能評価を行う．

発表資料

招待講演 13:30 - 15:00 座長：辻 尚史

ハイパフォーマンスコンピューティングからエッジコンピューティングへ - 宇宙開発における数値解析技術の今後 -

堤誠司（宇宙航空研究開発機構 研究開発部門第三研究ユニット）

概要

理論，実験に次ぐ第三の手法とされる数値解析は，ものづくりの革新を目指し，これまで数多くの研究が精力的に進められてきた．その結果，ロケットや航空機といった航空宇宙開発の現場ではもちろん，産業界においても設計ツールの1つとして使われるようになるほどに発展した．ものづくりを変革することを目指した数値解析術に関する研究は，富岳に代表される最新のスーパーコンピュータを利用し，今後も精力的に進めれる．一方，近年の宇宙開発では，深宇宙探査や月Gateway計画など，地上からの通信には遅延が大きいため，自律的な運用を可能とする技術が求められる．宇宙だけではなく，自動車や産業機器といった地上システムにおいても，IoT技術の発展と相まって，自律化への期待は大きい．本講演では，自律化を考えた上で見えてくるハイパフォーマンスコンピューティングの役割と，究極的にはエッジコンピューティングへ向けた数値解析技術の今後の方向性に関してご紹介する．

セッション5（処理系） 15:20 - 16:40 座長：小出 洋（九州大学）

Perl6 のサーバを使った実行

福田光希, 清水隆博, 河野真治 (琉球大学)

概要

Perl6 の実装の一つであるRakudoは, Byte code である MoarVM と, その上で動作する Perl6 のsubsetである nqp (Not Quite Perl) 上に構成されている,現状の Perl6 の実行は Perl6 で記述されたコンパイラを load して JIT しながら実行すること自体に時間がかかっている.そこで, Perl6 をサーバーとして動作させ, 実行するファイルをサーバーに投げて実行する方法を実装してみた.本論文では, サーバーで script 言語を実行する場合の利点と欠点について考察する.

発表資料

自由文思考プログラミング環境における手続的機能の実装

中村圭介 (ナレルシステム株式会社)

概要

日本語等で人間の本格的な思考をプログラミングできることを目指して述語論理等宣言的な知識の処理に適した独自処理系を開発している.一方,人間の本格的な思考に該当する手続的機能（本格的な数値計算や文字列計算）は,順次・分岐・反復制御等を用いた手続的なプログラミングのほうが,人間の動的な思考様式に対応して見通しもよく,アルゴリズムの工夫に応じて効率的となる場合も多い.そこで,標準的な論理プログラミング言語の手続的解釈における演算機能を手本にしながら,よりバックトラックの少ない独自処理系の性質を生かした比較文・制御構文・代入文・四則演算・文字列処理等を実装したので,これらについて紹介する.

発表資料

山内奨励賞表彰・受賞講演, スポンサー講演 ( トレジャーデータ株式会社 ) 17:00 - 18:10

山内奨励賞受賞論文1: 「ランダムな変異を用いたバグ入りプログラムの生成」寺田実 (電気通信大学)

受賞講演「乱数を使ってあれこれする話」寺田実 (電気通信大学)

概要

昨年の発表では、正しいプログラムにランダムに変異を加えることで 「ほとんどの場合正しく振る舞う」バグ入りプログラムの作成をこころみた。 はじめにその概要をふりかえったあと、同じように乱数を使っておこなった こころみについて紹介する。

山内奨励賞受賞論文2: 「並行プログラムのPartial Store Ordering での実行をモデル検査するためのRelease メモリバリア」鵜川始陽, 松元稿如, 飯干寛幸 (高知工科大学)

受賞講演「不揮発性メモリを使った永続化データ構造のモデル検査のためのライブラリ」鵜川始陽，飯干寛幸（高知工科大学）

概要

不揮発性メモリ（NVM）は電源が失われてもデータを保持でき，主記憶として 使えるメモリである．従来，データ構造を永続化する際は直列化して二次記憶 に格納していたところを，NVMを使えば，プログラム中で使っているデータ構造 をそのまま永続化できる．しかし，NVMを搭載したシステムでも，キャッシュ メモリから主記憶に書き戻されていないデータは永続化できない．キャッシュ キャッシュメモリの内容が主記憶に書き戻される順序は，プログラム中の書込み の順序と一致するとは限らない．そのため，NVMを使った永続化データ構造は， 慎重に設計しなければ，NVM上では一時的に不整合な状態になる．その時に 電源が失われると，データが復元できないので問題である．我々は，弱いメモリ 一貫性モデルでの並行プログラムの振舞いをモデル検査するためのライブラリ であるMMLibを開発している．本研究では，これを拡張してNVMを使った並行 データ構造をの振舞いを検査するライブラリを開発している．このライブラリ を使えば，MMLibが提供する書込み命令がキャッシュメモリに反映される順序 の非決定性に加えて，キャッシュメモリから主記憶に書き戻される順序の非決定性 を網羅して検査できる．

夕食 18:10 -

夜のセッション 19:30 -

第3日 1月12日

セッション6（教育） 9:00 - 10:20 座長：谷 聖一（日本大学）

オンラインプログラミング環境Google ColaboratoryにおけるPythonの導入実践例

山本周 (東京理科大学大学院)，清水克彦

概要

「情報I」の導入により，プログラミングが必修となった情報の授業では，文部科学省が公開した教員研修用教材でPythonが使用されており，採択される可能性が高い．そこでPythonによるプログラミング指導の効果の検討を目的とした．“Google Colaboratory”を用いたPythonの導入授業を行った．プログラミング経験者が1割程度である高校3年生に対して，計5時間の実施をした．“Google Colaboratory”を用いることで面倒な環境構築がなくなり，関連するライブラリのインストールも容易であった．また，実施したアンケートでは授業前に「プログラミングに興味があるか」に対して，「興味がある」が20.0％，「興味がない」が27.6％であった．計5時間授業を行った後に「プログラミングに興味を持ったか」に対して，「興味を持った」が51.0％，「興味を持たなかった」が16.6％などの結果を得た．“Google Colaboratory”によるPythonの指導は，導入なども含めて有用であることが分かった．アンケートの結果からは，生徒の興味を引くことができる等の結果を得た．

発表資料

プログラミング入門教育における短冊型問題の活用

久野靖 (電気通信大学)

概要

筆者らは2017年度から、プログラミング入門科目の試験において、完全自動採点の可能な「短冊型問題」(プログラムを行単位でばらばにして記号を付した選択肢とし、正しいプログラムに対応する記号列を解答させる問題形式)を用いており、その練習のため毎授業時冒頭に「確認テスト」を実施している。一方、学生の演習のようすを見ると、endの過不足、if文の外のelseの存在、returnの後に必要な文を置く、未定義変数の参照など、「基本的な間違い」が多く見られ、このような基本的な間違いを犯さないための学習支援の必要性を感じていた。そこで、正誤を見る試験とは別に、選択肢を並べてプログラムを完成させた状態で「アドバイス」ボタンを押すと基本的な間違いを指摘してくれるツールを作成し、2019年度から使用を開始した。本稿では、このツールの設計と実装および現時点での評価について述べ、このようなツールの有用性について検討した。実際にプログラミング入門科目の中でアドバイザを任意で使用でいるように提供した結果、アドバイザを使用して実際にアドバイスを取得した学生は約800人の授業登録者数のうち176名、そのうち3回以上の使用は77名であった。これらのうちから、授業時の確認問題を「手抜きでなく」受けている集団54名を抽出し、アドバイザを使用していない同様の学生と比較したところ、アドバイザが指摘するような誤りについて、有意に少なくなっていることが分かった。実際によく現れる基本的な誤りとしては、代入していない変数を参照する、メソッドの外に実行文があるなどのものが多かった。また、アドバイザの使用記録を時系列的に調べると、アドバイザを使用している学生は大半の指摘事項について、1回または2回の修正で解消できており、アドバイザが提供している指摘の説明はそれなりに分かりやすく効果的であるものと考えられる。

セッション7（パズル・ゲーム） 10:40 - 12:00 座長：山口 文彦（長崎県立大学）

MCTSを用いたタントリックスAIプレイヤーへの中盤の妨害戦略の実装と評価

長江恭英, 丸山一貴 (明星大学大学院情報学研究科)

概要

タントリックス・ストラテジーは，六角形のタイルを用いて線をつなげていく対戦型のゲームである．プレイヤーは自分の色の線で最長経路を作成することが目的となる．2016年には，対戦AIであるDarwinが人間のトッププレイヤーに勝利した．Darwinはモンテカルロ木探索を使用しているが，攻めの手を選びがちで，相手への妨害は考慮していない．そこでDarwinに対して中盤の妨害戦略を重点的に行うような実装を追加した．使用した戦略はコントロールサイドというもので，特定の場所に対するタイルの配置を制限することができる．実装後のプレイヤーはオリジナルに対して勝ち越すことができた．試合のログの分析結果から妨害状態を長く維持することが勝利に繋がることがわかった．妨害を長く続けることで相手の最長経路の延伸を阻止することが有効である．本稿では妨害の実装方法と試合の分析結果について述べる．

ゲームOtrioの3人および4人プレイの解析

松崎公紀(高知工科大学), 寺村舞童華

概要

Otrioは，2〜4人で行うボードゲームであり，4色 (3人プレイ時は3色) の駒を用いた立体三目並べと同様のゲームである．Otrioは，プログラミング・シンポジウムのGPCC（Games and Puzzles Competitions on Computers）の2019年の問題のひとつである．著者らは，これまでにOtrioの2人プレイの場合について解析を行い，第42回情報処理学会ゲーム情報学研究会 (2019年7月) において発表した．本研究では，3人プレイおよび4人プレイの場合について解析を行う．一般に，多人数ゲームでは二人ゲームと異なり，各プレイヤの選好順序（どのプレイヤを優先して勝たせたいか）とプレイヤ間の結託がゲームの勝敗に大きく影響する．そこで，本研究では特に結託のある場合について詳しく解析を行った．その結果，3人プレイでは，結託により勝つプレイヤを決定可能であること，4人プレイヤでは最初に着手するプレイヤが他のプレイヤと結託すると勝てることなどが分かった．

発表資料

閉会 12:00 - 12:10

Sponsored by トレジャーデータ株式会社

Sponsored by 株式会社インターネットイニシアティブ