著者

対馬 かなえ 浅井 健一

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.30, no.1, pp.1_180-1_186, 2013-01-25 (Released:2013-03-05)

---

本稿ではコンパイラに備わっている型推論器をそのまま使い,型デバッガを作成する手法について述べる.これまでの型デバッガでは型推論器を独自に再実装して型を求めていたが,それらの手法と比較して我々の手法には3つの利点がある.1つ目は型推論結果に不一致が起きないことが保証されることである.従来の型デバッガでは,型デバッガの型推論器とコンパイラの型推論器の間で齟齬が起きる可能性があった.2つ目はそもそも型推論器を再実装する必要がないことである.それによりこれまでに行われていない,構文等が多い言語の型デバッガを容易に作成することが出来る.3つ目はコンパイラの型推論器の更新に依存しないことである.これらの利点を活かし,我々は実際にOCamlを対象とした型デバッガを実装した.本稿では単純型付きラムダ計算とlet多相を対象として提案手法を説明し,実装について述べる.

著者

寺田 秀樹 仲野 公章 浅井 健一 山越 隆雄 金子 正則 石井 靖雄

出版者

社団法人 砂防学会

雑誌

砂防学会誌 (ISSN:02868385)

巻号頁・発行日

vol.53, no.3, pp.52-57_2, 2000

---

An earthquake measuring 6.4 in Magnitude (M) on the Richter scale occurred at 16:02 on July 1, 2000, with an epicenter in the sea near Niijima and Kozushima Islands in the Izu island chain. It was followed by torrential rainfall caused by typhoon No.3 in July 7 and 8, and another earthquake measuring M 6.0 at 3:57 on July 9, with a hypocenter near the previous earthquake. They triggered many slope failures in Kozushima Island. The slope failures damaged some houses, and also produced a large amount of sediments on the beds of many streams.<br>In order to assess the risk of sediment-related disasters, the team of Erosion and Sediment Control Department in Public Works Research Institute has surveyed the state of slope failure deposits and erosion and sediment control facilities. The results of the surveys from July 4 to 6 and July 10 to 11 are as follows. 1) Slope failure sediments on the streambeds increase danger of debris flow disasters, because these streams have few erosion and sediment control facilities, except for Kozusawa. 2) Many slope failures and a few landslides were recognized in the surveyed area. Many of these failures occurred in the area of pyroclastic deposits. 3) The torrential rainfall by typhoon No.3 and the earthquake in July 9 widen the area of slope failure caused by the earthquake in July hand also caused new failures. It suggests that additional rainfall or earthquake will cause new failures and area extention of the failures which already occurred.

著者

千葉 達朗 林 信太郎 小野田 敏 栗原 和弘 藤田 浩司 星野 実 浅井 健一

出版者

一般社団法人 日本地質学会

雑誌

地質学雑誌 (ISSN:00167630)

巻号頁・発行日

vol.103, no.6, pp.XXI-XXII, 1997 (Released:2010-12-14)

被引用文献数

1

---

5月11日午前8時, 秋田県鹿角市の澄川温泉で, 地すべりと石流が発生, 澄川温泉と赤川温泉の16棟が全壊, 国道341号も寸断された. 5月4日頃から水の濁りや道路の変状等が察知され, 適切な警戒避難が行われたため, この災害による死者・負傷者はなかった. なお, 地すべりの最中に末端付近で水蒸気爆発が発生した. ここでは, 5月12日にアジア航測(株)が撮影した空中写真, その後の現地の他, 秋田航空(株)が撮影した水蒸気爆発の瞬間の写真を紹介する.

著者

河内谷 清久仁 浅井 健一

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.28, no.4, pp.4_63-4_68, 2011-10-25 (Released:2011-12-25)

著者

阪上 紗里 浅井 健一

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

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

---

「プログラムの残りの計算」を表す継続を扱う為の基礎言語体系として,対称λ計算(Symmetric λ-calculus, SLC)がFilinskiによって提案されている.SLCにおいては項と継続が完全に対称な形をしており,項を扱うのと同じように継続を扱うことができる.そのため,項と継続を統一的に議論するのに適していると思われるが,これまでSLCについての研究はほとんどなされていない.ここでは,まずSLCをsmall step semanticsで定式化し直し,型付き言語の基本的な性質であるProgressとPreservationを満たすことを証明する.次に,SLCが継続計算を議論・表現するのに適していることを示すため,(1) FelleisenのCオペレータを含むcall-by-value言語,ΛC計算,および(2) Parigotのcall-by-name λμ計算が,どちらも自然にSLCに変換できることを示す.近年call-by-valueとcall-by-nameの双対性が項と継続の対称性と絡めて注目されているが,ここでの結果はそれに対する洞察を与えるものと期待される.

著者

叢 悠悠 浅井 健一

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.36, no.2, pp.2_47-2_60, 2019-04-26 (Released:2019-06-25)

---

CoqやAgdaなどの定理証明支援系では,依存型を使ってプログラムの性質を正確に記述することができる.一方,依存型付き言語の多くは,副作用を許さないという制約もつ.これは,副作用の動的な振る舞いによって型が静的に定まらなくなることによるが,副作用の欠如は実用的なプログラムの実装の妨げとなるため,適切な制約を設けながら,依存型付き言語に副作用を導入する試みがなされてきた.本研究では,限定継続命令 shift/resetをもつ依存型付き言語を考える.shift/resetはさまざまな副作用の模倣を可能にするが,その応用例や型システムは単純型付き言語で考えられてきた.本稿では,shift/reset と依存型を組み合わせるために必要な制約を明らかにし,健全な型システムを定義する.また,設計した言語に対するCPS変換を与え,変換が型を保存することを証明する.

著者

千葉 達朗 林 信太郎 小野田 敏 栗原 和弘 藤田 浩司 星野 実 浅井 健一

出版者

日本地質学会

雑誌

地質學雜誌 (ISSN:00167630)

巻号頁・発行日

vol.103, no.6, pp.XXI-XXII, 1997-06-15

被引用文献数

4 1

---

5月11日午前8時, 秋田県鹿角市の澄川温泉で, 地すべりと石流が発生, 澄川温泉と赤川温泉の16棟が全壊, 国道341号も寸断された. 5月4日頃から水の濁りや道路の変状等が察知され, 適切な警戒避難が行われたため, この災害による死者・負傷者はなかった. なお, 地すべりの最中に末端付近で水蒸気爆発が発生した. ここでは, 5月12日にアジア航測(株)が撮影した空中写真, その後の現地の他, 秋田航空(株)が撮影した水蒸気爆発の瞬間の写真を紹介する.

著者

叢悠悠 浅井健一 戸次大介

雑誌

研究報告自然言語処理(NL)

巻号頁・発行日

vol.2013-NL-214, no.19, pp.1-6, 2013-11-07

---

プログラミングにおける 「継続」 とは,残りの計算,すなわちある部分項に対する文脈のことを指す.この概念を自然言語の意味論に取り入れることで,様々な言語現象の意味を記述することができる.本研究では,限定継続命令 shift/reset を用いた副詞 only のフォーカスの分析 (Bekki and Asai (2010)) を OCaml で実装し,一つのフォーカスを含む文の意味表示を正しく計算できることを確認した.しかし,フォーカスが複数存在する場合への非対応など,今回の実装にはいくつかの問題があり,それらについても考察する.

著者

浅井 健一

出版者

東京大学

雑誌

奨励研究(A)

巻号頁・発行日

1997

---

自己反映言語のコンパイルを目指して、おもにその基礎技術である部分評価法の研究を行った。部分評価器を自己反映言語のコンパイラとして使用するためには、使用する部分評価器が(1)十分、強力で、かつ(2)効率的に動くこと、の2点が重要である。これらに対応して以下のような結果を得た。1. 部分評価器の能力として、構造データをきちんと扱えることが重要で、そのためには部分評価時に各式の値とコードの両方を保持することが重要であることを発見した。これに基づいて実際にonlineの部分評価器を作成し、その効果を確かめた。しかし、この方法はonlineのため効率に問題があることがわかった。2. より効率的な部分評価を実現するべく、上記の方法をofflineに拡張する方法を提案した。この方法は、構造データをうまく扱う特化器の作成と束縛時解析器の作成というふたつの部分からなる。このうち前者は、必要に応じて値とコードの両方を保持し、かつコードの複製を避けるためコード部分を必ずlet式に残すことでうまくできることがわかった。この特化器を使って実際にいろいろな特化を行い、自己適用によるコンパイラジェネレータの作成を含めてうまく動くことを確認した。後者に関しては、従来の束縛時解析の手法を拡張することで、値とコードの両方を持つべき場所を特定できることを示した。その過程で、束縛時解析は、比較的、素直に制約を生成する型システムとして定式化できるが、制約を解くためには従来の手法と違い、2段階にわける必要があることがわかった。束縛時解析は実際に実装を行い、うまく動くことを確認した。今後の課題としては、ここで提案した束縛時解析の多段の部分評価への応用、今回は行うことができなかった自己反映言語のコンパイルへの実際の適用などがあげられる。

著者

木谷 有沙 浅井 健一

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.27, no.3, pp.3_51-3_66, 2010-07-27 (Released:2010-09-27)

---

本研究では,限定継続処理shift/resetを含むλ計算の,正当性の保証され,かつ機械語により近い実装を得ることを目指している.その手法として,shift/resetを定義するCPSインタプリタに対し,変換前後の評価器の等価性が保証されている変換のみを用いて抽象機械及び遷移規則を得る.これはDanvyらによって提案された手法に則っており,本論文でも同様のCPS変換,非関数化を最初に行っている.ただし,より実際の機械語実装に近づけるために,スタック導入と環境退避という二つの新しい変換を導入した.本論文ではこれらの変換の概要と変換前後の等価性について触れる.これらの変換の結果,CPSのインタプリタに妥当なプログラム変換のみを用いて,スタックへの環境退避を行う抽象機械を得られることが分かっている.今後,この抽象機械に他の妥当な変換を更に施すことで,既存の機械語に類似した命令セットを処理する機械が得られると考えている.

著者

小峯 健一 浅井 健一 板垣 昌志 小峯 優美子 黒石 智誠 阿部 省吾 阿部 榮 齋藤 博水 熊谷 勝男

出版者

公益社団法人 日本畜産学会

雑誌

日本畜産学会報 (ISSN:1346907X)

巻号頁・発行日

vol.70, no.9, pp.169-176, 1999-08-25 (Released:2008-03-10)

参考文献数

36

被引用文献数

1

---

健康な乳牛の泌乳期から乾乳,分娩期に及ぶ各ステージの乳房総計68例から乳汁を採取し,それぞれの体細胞数(SCC)とこれらの細胞が中心的に産生する生理活性タンパク分子である,ラクトフェリン(Lf),αl酸性糖タンパク(α1AG),フィブロネクチン(FN)の各濃度を測定した.さらには乳腺内リンパ球の産生するIgG1とIgG2を中心とした,免疫グロブリン(Ig)サブクラスの濃度を測定し,それぞれの変動を追跡した.その結果,SCCは泌乳期の間は低値を示したが,乾乳導入後いち早く増加した.このSCCの上昇に伴って,最も早期にLfの産生が起こり,これに続いて,αlAGやFN値も上昇し,いずれも乾乳期中期までには最高値に達した.一方,乳汁中のIg濃度は,泌乳期を通じて乾乳初期まで低値を示していたが,乾乳中期に移行するに及びIgG1を主とした濃度の急速な増加を示し,初乳分泌期である乾乳後期には極めて高値のG1/G2比(60-7)と共に,最高濃度を示した.以上の成績は,乾乳導入に伴う乳腺分泌液へのSCの集積と,それに続く生理活性タンパク分子の急速な産生は,泌乳期乳腺上皮細胞の退行と新しい乳腺組織の増殖分化を営むために必須で,また,次回分娩に備えたIgG1を主体とした乳腺内での初乳形成を促進する生理的変化であることを示唆した.

著者

宮沢 孝幸 坂口 翔一 小出 りえ 谷利 爵公 入江 崇 古谷 哲也 水谷 哲也 神道 慶子 野田 岳志 桑原 千恵子 酒井 沙知 浅井 健一 川上 和夫

出版者

京都大学

雑誌

挑戦的萌芽研究

巻号頁・発行日

2016-04-01

---

これまで猫の腎炎とウイルスの関係に注目した研究はほとんどなかった。しかし、2012年に香港で尿細管間質性腎炎と関連するネコモルビリウイルス(FeMV)が発見された。FeMVはパラミクソウイルス科モルビリウイルス属に分類されるウイルスで、猫の尿や糞便から検出されている。アジア、ヨーロッパ、アメリカの様々な国でFeMVの検出がなされていることから、同ウイルスは世界中に広まっていると考えられている。しかし、その一方でこのウイルスの病原性発現機構は不明である。そこで本研究においては、FeMV感染時の宿主の免疫応答に着目し、FeMV感染とウイルス性腎炎の関係を明らかにすることを目的として研究を行った。

著者

門脇 香子 浅井 健一

雑誌

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

巻号頁・発行日

vol.2015, pp.115-120, 2015-01-09

---

Agda はマルティンレフの型理論に基づいた定理証明支援器であり,その一方で依存型をもつ関数型プログラミング言語でもある.Agda では依存型 (Dependant Types) を用いることができるのも大きな特徴である.また,定理証明支援器とプログラミング言語両方の特徴をもちあわせていることから,何かを実装しつつ証明するのに適している.そこで本稿では,停止性が保証された型推論器を Agda により構成する.なかでも, Unification の実装では, McBride の手法を採用する.これは型変数の数を巧妙に管理することで構造に従った再帰を使って(つまり停止性が明らかな形で)型の Unification を表現できることを示したものである.本稿では Term の型変数の数に注目しつつ,主に Unification の部分と Application の実装にフォーカスを当てながら実装していく.

著者

阪上 紗里 浅井 健一

出版者

Japan Society for Software Science and Technology

雑誌

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

巻号頁・発行日

vol.26, no.2, pp.3-17, 2009-04-24

---

「プログラムの残りの計算」を表す継続を扱う為の基礎言語体系として,対称λ計算(Symmetric λ-calculus, SLC)がFilinskiによって提案されている.SLCにおいては項と継続が完全に対称な形をしており,項を扱うのと同じように継続を扱うことができる.そのため,項と継続を統一的に議論するのに適していると思われるが,これまでSLCについての研究はほとんどなされていない.ここでは,まずSLCをsmall step semanticsで定式化し直し,型付き言語の基本的な性質であるProgressとPreservationを満たすことを証明する.次に,SLCが継続計算を議論・表現するのに適していることを示すため,(1) FelleisenのCオペレータを含むcall-by-value言語,Λ<SUB>C</SUB>計算,および(2) Parigotのcall-by-name λμ計算が,どちらも自然にSLCに変換できることを示す.近年call-by-valueとcall-by-nameの双対性が項と継続の対称性と絡めて注目されているが,ここでの結果はそれに対する洞察を与えるものと期待される.

著者

貝 健三 小峯 優美子 小峯 健一 浅井 健一 黒石 智誠 小堤 知行 板垣 昌志 太田 實 熊谷 勝男

出版者

社団法人日本獣医学会

雑誌

The journal of veterinary medical science (ISSN:09167250)

巻号頁・発行日

vol.64, no.10, pp.873-878, 2002-10-25

被引用文献数

6 23

---

乾乳早期のブドウ球菌性乳房炎に罹患したホルスタイン種の乳牛に対して,ウシラクトフェリンの臨床効果を評価した.3農場でブドウ球菌性乳房炎を発症した41分房から無作為に選定した12分房にはウシラクトフェリンを投与し,29分房には対照として抗生剤を投与した.その結果,ウシラクトフェリン投与区では91.7%の乳房炎分房が分娩後7日目までに治癒し,対照区では48.3%が治癒した.別の分房を用いて乳汁の変化を調べたところ乳房炎分房における乳汁中のブドウ球菌数は,ウシラクトフェリンを投与した5分房および抗生剤を投与した対照の5分房において,投与後,有意に減少した(p<0.05).この乳汁における全細胞数は,ウシラクトフェリンを投与した分房では増加したが,対照分房では変化が認められなかった.また,健康な乳房においてもウシラクトフェリンを投与した6分房に限って,乳汁中全細胞数が増加し,これらの細胞の多くは多形核白血球および補体受容体であるCD11bの陽性細胞といった食細胞群であった.乳房炎分房における乳汁中C3濃度はウシラクトフェリンを投与した5分房で有意に増加したが(p<0.05),対照の5分房では投与後の有意差は認められなかった.以上の結果より,ウシラクトフェリンによる治療には乾乳早期のブドウ球菌性乳房炎に対して宿主の自然免疫を誘導し,乳房炎の治癒率が高まる可能性が示唆された.

著者

浅井 健一 松岡 聡 米澤 明憲

雑誌

全国大会講演論文集

巻号頁・発行日

vol.41, pp.8-9, 1990-09-04

---

近年、並列Lispが関数型言語の潜在的な並列性を大きく引き出せるものとして注目されている。実際にMultilisp[3]をはじめとしてMultischeme[6],Mul-T[5],QIisp[2]などたくさんの並列が開発され並列計算機上で高い性能が報告されている。しかし、現在のところ並列Lispは並列計算機上での性能を向上させることを目的としているのでもっぱら性能に関しての議論がなされ、言語の意味に関する考察はほとんどなされていない。そのため言語仕様があいまいになるし、言語仕様の変更も難しくなっている。このことはスケジューリング方式の固定化を引き起こし、ひいては自己反映計算[8]の実現を難しくしている。そこでMultiLispの操作的意味記述[1]を与え、これを用いて逐次型計算機上にSchme[7]によるインタプリタを作成した。さらにこれをもとに表示的意味記述を与える。またその記述から導かれるfutureとcall/ccとの相互干渉について述べる。