著者

門脇 香子 浅井 健一

雑誌

第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との相互干渉について述べる。

著者

金寺 登 荒井 隆行 岡田 賢治 浅井 健司

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会技術研究報告. SP, 音声 (ISSN:09135685)

巻号頁・発行日

vol.103, no.155, pp.67-72, 2003-06-20

---

音声特微量の時間軌跡をフーリェ変換したものは変調スペクトルと呼ばれ,音声の認識には特定の変調スペクトルが重要であることが知られている.本報告ではよ音声認識にとって変調スペクトルの各成分がどの程度重要であるかを示す貢献度に応じて変調スペクトルを強調した音声認識特微量を提案する.自動音声認識実験の結果,提案した特微量は,雑音環境下において音声認識性能が約5%改善されることを確認した.

著者

小黒 康正 浅井 健二郎 小黒 康正 杉谷 恭一 小川 さくえ 増本 浩子 桑原 聡 恒吉 法海 東口 豊 恒吉 法海 福元 圭太 杉谷 恭一 小川 さくえ 坂本 貴志 増本 浩子 濱中 春 山本 賀代 岡本 和子 北島 玲子 桑原 聡 クラヴィッター アルネ オトマー エーファ

出版者

九州大学

雑誌

基盤研究(B)

巻号頁・発行日

2006

---

ドイツ現代文学は、言語に対する先鋭化した批判意識から始まる。とりわけホーフマンスタール、ムージル、カフカの文学は、既存の言語が原理的機能不全に陥っていることを確信しながら、言語の否定性を原理的契機として立ち上がっていく。本研究は、ドイツ近・現代文学の各時期の代表的もしくは特徴的な作品を手掛かりとして、それぞれの作品において<否定性>という契機の所在を突き止め、そのあり方と働きを明らかにした。

著者

松浦 純 浅井 健二郎 平野 嘉彦 重藤 実 イヴァノヴィチ クリスティーネ 浅井 健二郎 西村 雅樹 藤井 啓司 松浦 純 冨重 純子

出版者

東京大学

雑誌

基盤研究(A)

巻号頁・発行日

2003

---

この研究では、4年間で計9回の研究会を開催し、のべ63名から研究成果の報告を受け、討論を行った。トピックは次のようなものであった。・記憶と身体に関する研究・記憶のメディア、メディアと記憶に関する研究・集合的記憶と文化的アイデンティティーに関する研究・記憶と意識、記憶と無意識、記憶と忘却に関する研究・記憶と痛みに関する研究これらのトピックに関して、具体的な分析対象として取り上げられたのは、ヘルダーリン・ニーチェ・リルケ・カフカ・ベンヤミン・フロイト・レッシング・マン・ゲーテ・グリルパルツァーなどの作家・批評家たちである。これまでの研究から、広義の「記憶」にあたるドイツ語の類義語はさまざまあり、ドイツ文学に表現された記憶の系列は多岐にわたっていることが明らかになった。記憶とはもともと過去に由来するものだが、文学テクストにおける記憶は、過去・現在・未来という直線的な時間観念とは異なった時間を内包している。また記憶とは元来は個人の機能であるはずだが、その記憶を保ち続けることにより、記憶が集合的な歴史へと拡大されるシステムを持つことも明らかになった。特に「痛み」の記憶は、個人にとっても社会にとっても忘れがたいものであり、文学テクストにおいても痛みの聖化・神秘化・倒錯など、さまざまな表現形式が存在する。これまでに明らかになった上記のような研究成果をまとめ、さらに今後研究を進めることが必要だと思われる点を検討した。特に「痛み」という文化ファクターの視点からドイツ文学における表現形式を検討することは、この研究では十分にはできなかったので、今後の重要な課題として残ることになった。