著者

ケイ アラン・カーティス 林 康史 中野 圭介 筧 一彦

出版者

一般社団法人日本ソフトウェア科学会

雑誌

コンピュータソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.22, no.4, pp.65-83, 2005-10-26

著者

中野 圭介 増見 伸 中村 浩一 中野 吉英

出版者

公益社団法人 日本理学療法士協会

雑誌

理学療法学Supplement Vol.41 Suppl. No.2 (第49回日本理学療法学術大会 抄録集)

巻号頁・発行日

pp.1374, 2014 (Released:2014-05-09)

---

【はじめに,目的】パルスオキシメーターは非侵襲性を特徴とし,簡易的にセンサーを装着するだけで,連続的かつリアルタイムに経皮的酸素飽和度(以下,SpO2)をモニタリングすることが可能である。センサーの種類には手指に装着する透過型の指尖部センサー,前額部に軽く圧迫を加え固定する反射型の前額部センサーなどがある。なかでも前者は,指先に装着できることから,一般・救急外来,集中治療室,手術室をはじめ,リハビリテーションの現場においても広く用いられている。しかし,手指の障害や体動が激しい場合などには,足趾に装着されるケースも少なくない。これまで,実際の患者での吸痰操作において前額部,耳朶,手指の順にSpO2が低下し,各装着部位で同様の変動傾向があったことを報告した研究はあるものの,足趾と他部位の関係性を検討した研究は我々が探索する限り見当たらない。そこで本研究では,まず手指と足趾におけるSpO2低下度合いの相違およびSpO2が最も低下するまでに要する時間差(タイムラグ)を比較検討し,さらに身体・検査データからSpO2測定に影響を及ぼす関連因子を検討することで,手指・足趾におけるSpO2測定の特性および有用性を明らかにすることを目的に実施した。【方法】対象は循環器障害および上下肢に形態的変化の既往が無い健常な男性33名とし,平均年齢27.0±2.9歳,身長171.8±10.6cm,体重66.2±3.4kgであった。すべての被験者は,ベッド上背臥位にて5分間の安静を行った後,最大呼気に引き続き30秒の息こらえを行った。その後,手指および足趾のSpO2を経時的に追い,最も低下した時点でのSpO2(以下,最低SpO2)および最大呼気終了後から最も低下した時点までに要した時間(以下,所要時間)を測定した。測定する手指および足趾は右側の第2指とし,測定機器にはPumoRi7165(ユビックス株式会社製)を用いた。なお,測定肢位は解剖学的肢位とし,室温を25℃,時間を健康診断直前に設定し,外光などにも注意を払った。身体・血液データは健康診断で得られた情報を基とし,血液通過時間に影響を与える因子である肥満度(身長・体重・BMI),血圧(収縮期血圧・拡張期血圧),赤血球変形(赤血球数・血色素量・赤血球容積),動脈硬化・高脂血症(総コレステロール・低密度リポたん白質・高密度リポたん白質・中性脂肪)を選択した。統計手法は最低SpO2,所要時間ついてPaired t-testを用いて比較検討した。さらに,最低SpO2および所要時間,身体・血液データについてPearsonの相関係数により検討した。なお,それぞれの統計学的処理について有意差の判定は危険率5%未満とした。【倫理的配慮,説明と同意】本研究はヘルシンキ宣言に基づき,全対象者に対して研究の主旨,内容について口頭および紙面にて十分に説明し,同意を得た上で研究を開始した。【結果】最低SpO2は手指89.3±4.9%,足趾90.8±5.6%,また所要時間は手指50.5±6.3秒,足趾62.9±10.1秒であった。手指と足趾の最低SpO2の比較において,有意差が認められず,手指と足趾における最低SpO2の相関では正の相関関係が認められた(r=0.80,p<0.001)。所要時間の比較において,足趾は手指と比べ有意に遅延していた(p<0.01)が,有意な相関関係は認められなかった(r=0.28,p>0.05)。手指所要時間と身体・血液データの相関において,手指所要時間は身長との間に正の相関関係(r=0.39,p<0.05)が認められ,血色素量・赤血球容積との間に負の相関関係(r=-0.42・r=-0.43,p<0.05)が認められた。【考察】手指と足趾における最低SpO2の比較では,有意差が認められず,手指と足趾の間に正の相関関係が認められた。このことから,足趾で測定する場合も手指測定と同様の結果が推測できるため,足趾測定における評価の有用性が示唆された。しかしながら,所要時間の比較において足趾は手指と比べて有意に遅延し,また有意な相関関係は認められなかったことから,足趾でのSpO2測定では,これら特性を考慮する必要がある。手指所要時間と身体・血液データの相関において,手指所要時間は身長との間に正の相関関係,血色素量・赤血球容積との間に負の相関関係が認められたことから,身長が高いほど,また血色素量・赤血球容積が低値であるほど,所要時間が遅延する可能性が示唆された。【理学療法学研究としての意義】本研究は手指・足趾間におけるSpO2の有用性と関連因子について検討し,一定の見解を得ることができた。この結果をもとに,理学療法評価の一助となることを期待したい。

著者

高橋 祐多 中野 圭介

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.35, no.4, pp.52-71, 2018-10-25 (Released:2018-12-26)

---

一般に関数の等価性判定問題は決定不能であるが,関数の定義に構文的な制約を加えることで決定可能にすることができる. そのような制約の 1 つとして,木から文字列への決定性トップダウン変換(deterministic top-down tree-to-string transducer,yDT)が存在し, 等価性判定が決定可能な関数としては,比較的広い範囲のものを扱うことができる. この yDT の等価性判定の決定可能性は 2015 年に Seidl らによって示されたが,2 つの半アルゴリズムを組み合わせることによって証明されており, 計算量が特定できず,実用性が確認されていない. そこで,本論文では yDT の等価性判定を行うプログラムを実装し,Seidl らの等価性判定アルゴリズムが実用に堪えうるものか検証する.

著者

中野 圭介

雑誌

第54回プログラミング・シンポジウム予稿集

巻号頁・発行日

vol.2013, pp.181-188, 2013-01-11

---

関数型プログラミングにおいて,リストを消費する関数 foldr および生成する関数 unfoldr は重要な役割を果たす.特に,入力を foldr によって消費し,出力を unfoldr によって生成するような関数はメタモルフィズムとよばれ,基数変換などに代表される或るデータ表現から別のデータ表現への変換を自然に定義することが可能である.Bird と Gibbons は,このメタモルフィズムに対し,入力を消費しながら出力を生成するようなストリーム処理として実装できるための条件を提示したが,自然数に対する基数変換には応用することができなかった.これは入力の桁を全て読み込まない限り,出力の桁を決定できないためで,彼らの提示した条件を満たしていない.これを解決するために著者が提案した手法が,ジグソーパズルを利用したメタモルフィズムの計算機構である.本稿では,グレイコードのような特別な記数法に対してこの機構を適用し,対応するジグソーモデルの導出方法を示す.

著者

阿部 和敬 中野 圭介

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.12, no.2, pp.14, 2019-05-21

---

マクロ木変換器(MTT)とは,入出力を木構造とする累積引数付き再帰関数のモデルである.複数のMTTの合成として表現される関数を,1つのMTTで表現することをMTTの融合という.一般にはMTTを融合できるとは限らないが,特定の条件下では融合手法が知られている.VoigtländerとKühnemannは,入力木のコピー回数に関する条件を満たす2つのMTTの融合手法を示した.ただし,1つのMTTで表現できるにもかかわらず,彼らの手法を繰り返すことでは融合できない3つ以上の合成も存在する.Manethは,任意の個数のMTTの合成が最終的な出力木のサイズに関する制約を満たすとき,合成に相当する1つのMTTが構成できることを証明した.しかし,彼の研究は融合可能性の証明が目的のため構成は煩雑である.そこで本発表では,高階木変換器(HTT)を用いてVoigtländerとKühnemannの手法を一般化し,Manethの証明に実用に向いた別証明を与える.HTTとは,MTTの一般化として提案された高階関数のモデルである.本融合は,まずMTTの合成を1つのHTTとして表現し,HTTに現れる高階関数のオーダを下げていくことで,MTTへの融合を実現する.理論上融合が不可能な場合でも,本融合は合成に相当する1つのHTTを得ることができる.

著者

阿部 和敬 中野 圭介

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.12, no.2, pp.14, 2019-05-21

---

マクロ木変換器(MTT)とは,入出力を木構造とする累積引数付き再帰関数のモデルである.複数のMTTの合成として表現される関数を,1つのMTTで表現することをMTTの融合という.一般にはMTTを融合できるとは限らないが,特定の条件下では融合手法が知られている.VoigtländerとKühnemannは,入力木のコピー回数に関する条件を満たす2つのMTTの融合手法を示した.ただし,1つのMTTで表現できるにもかかわらず,彼らの手法を繰り返すことでは融合できない3つ以上の合成も存在する.Manethは,任意の個数のMTTの合成が最終的な出力木のサイズに関する制約を満たすとき,合成に相当する1つのMTTが構成できることを証明した.しかし,彼の研究は融合可能性の証明が目的のため構成は煩雑である.そこで本発表では,高階木変換器(HTT)を用いてVoigtländerとKühnemannの手法を一般化し,Manethの証明に実用に向いた別証明を与える.HTTとは,MTTの一般化として提案された高階関数のモデルである.本融合は,まずMTTの合成を1つのHTTとして表現し,HTTに現れる高階関数のオーダを下げていくことで,MTTへの融合を実現する.理論上融合が不可能な場合でも,本融合は合成に相当する1つのHTTを得ることができる.Macro tree transducers (MTTs) are models for recursive functions (with accumulating parameters) on tree-structured data. Constructing a single MTT equivalent to a composition of given MTTs is called 'fusion' of the MTTs. Although it is not always possible to fuse given MTTs in general, fusion methods under certain conditions are known. Voigtländer and Kühnemann showed a fusion method of two MTTs restricted about the number of copying an input tree. However, a repetition of their method cannot necessarily fuse more than two MTTs even in the case where there exists a single MTT equivalent to the composition of them. Maneth proved that we can construct an MTT equivalent to a composition of given multiple MTTs restricted about the size of final output trees. However, since he is interested only in the fusibility, the construction is complicated. This presentation gives another proof adapted to practical uses for Maneth's proof as a generalization of Voigtländer and Kühnemann's method with high-level tree transducers (HTTs). Htt was proposed as a generalization of MTT, which is a model of higher-order functions. Our fusion method comprises two steps: first, a single HTT is obtained as a composition of given multiple MTTs; then, the orders of functions are lowered as much as possible. In this approach, we can obtain a 'fused' HTT even where there is no single MTT equivalent to the composition of MTTs.

著者

小澤 祐也 中野 圭介

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.12, no.2, pp.12, 2019-05-21

---

定理証明支援系Coqでは,無限に続くリストのような余帰納的構造を持つデータについての証明を,タクティクと呼ばれるコマンドを用いて進めることができる.ただ,Coqでは無限のデータや証明をそのまま扱うことはできないため,再帰的な表現による有限の形で表している.このような無限のデータや証明は再帰関数として表現されるため,意味のないループの形でないという,ガード条件の検査(guardedness check)が証明の最後に行われている.このため証明全体を走査するために時間がかかってしまうという問題や,途中でガード条件が成立しなくなっていてもユーザは証明の最後の検査まで気づくことができないという問題がある.Coqには証明途中でガード条件の検査を行うGuardedコマンドが存在するが,これもそれまでの証明全体を走査するために,タクティクごとに実行すると時間効率が悪い.そこで本発表では,Coqにおける余帰納的証明のガード条件の検査を証明中に少しずつ行い,ガード条件が成立しなくなった際,即座にユーザに知らせることができるような手法を提案する.本手法ではタクティクの実行ごとに新しく作られた部分の証明のみを取得し,その部分的な証明に対してガード条件の検査を行う.検査を行った後は,その時点での環境やゴールのIDなどの情報を保持しておき,次回のタクティク実行時のガード条件の検査に用いる.

著者

松田 一孝 胡 振江 中野 圭介 浜名 誠 武市 正人

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.26, no.2, pp.2_56-2_75, 2009-04-24 (Released:2009-06-24)

---

双方向変換は,元のデータの一部を抽出し加工する順方向変換と,順方向変換で得られたデータに対する変更を元データに書き戻す逆方向変換の二つの変換から構成される.双方向変換を用いることで,XML文書の同期や相互変換を行える.さらには,双方向変換はプレゼンテーション指向の文書作成やソフトウェアエンジニアリングにも利用できる.著者らは2007年に,順方向変換を記述するプログラムが与えられたときに自動的に逆方向変換を得る系統的な手法を提案した.しかし,そこで扱われている順方向のプログラムは制限が強く,制限の一つとして変数を二度以上使用することが禁止されていたため,複製を含む変換は記述できなかった.そこで本論文では,前手法を拡張し,複製を含むプログラムにおいても自動的に逆方向変換を得る手法を提案する.

著者

中野 圭介

雑誌

第54回プログラミング・シンポジウム予稿集

巻号頁・発行日

vol.2013, pp.181-188, 2013-01-11

著者

田代 克也 中野 圭介 岩崎 英哉

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.6, no.3, pp.51-51, 2013-12-20

---

Webアプリケーションの開発を支援するための枠組みとして,テストツールと呼ばれる機能が多くの開発フレームワークにおいて提供されている.この機能では,テストに必要な入力値などの組であるテストケースを開発者が設定することで,自動的なテストの実行が可能である.しかしながら,正確なテストを行うには,入力値などを詳細に記述しなければならないため,テストケースの作成自体が開発者側への大きな負担となっている.本発表では,Webアプリケーション開発フレームワークにおける,テストケースの自動生成機能を提案し,実装を行った.対象とする開発フレームワークは,現在主流になっているRuby on Railsとし,Railsのテストツール機能の1つである機能テストにおいて実装した.本システムでは,開発者は全体の入力値の一部を与えることで,不足している入力値を補完しつつテストケースが生成される.また,オープンソースのRailsのWebアプリケーションに対して本システムを適用し,多くのテストケースが自動生成されることを確認した.Many Web application frameworks provide testing tools for supporting development of Web applications. The testing tools automatically test a Web application with a set of test cases given by a developer. However, the developer should carefully designate the set of test cases to achieve precise tests. We propose and implement an automatic test case generation system for a Web application framework. Our system works for the Web application developed with Ruby on Rails which is widely used. It provides a set of test cases for functional tests on Rails from only a part of input values designated by a developer. Furthermore, we demonstrate that our system can automatically generate many test cases for open-sourced Web applications developed with Rails.

著者

岩崎 英哉 中野 圭介 鵜川 始陽

出版者

電気通信大学

雑誌

基盤研究(C)

巻号頁・発行日

2011

---

本研究は,サーバ側で実用的な性能で動作する サーバサイドJavaScript処理系を開発することにより,煩雑な Web アプリケーション開発のコストを大きく低減させることを目指し,以下の成果を得た.(1) プログラムの実行情報を利用した最適化を行い実行速度を向上させるJavaScript処理系を構築した.(2) JavaScriptプログラムとC言語で記述されたプログラムとの連携を可能とする機構を構築した.(3) イベント駆動方式サーバのための並列JavaScript処理系を設計し実装した.(4) JavaScriptプログラムの安全な実行の基礎となる型システムを構築した.