著者
坂口 和彦 亀山 幸義
雑誌
情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)
巻号頁・発行日
vol.10, no.1, pp.14-28, 2017-01-06

本研究は,対話的定理証明器Coqの有限型と有限ドメイン関数に関する既存ライブラリを改良し,従来のライブラリを用いた証明をほとんど変更することなく,その証明から抽出されるプログラムの効率を大幅に改善したものである.CoqのSSReflect/Mathematical Componentsライブラリは,有限型と有限ドメイン関数をサポートするライブラリfintypeとfinfunを提供し,これらのデータに対する証明の手間を大幅に削減することに成功している.しかし,その証明からプログラム抽出の手法で作成したプログラムは,多くの場合において非常に効率が悪いという問題がある.本研究では,fintypeやfinfunを改善したライブラリを実装した.このライブラリを用いて作成した証明から抽出したOCamlコードは,既存ライブラリの場合と比べて非常に高速である.例として,行列積の計算では,計算時間をおよそO(n5)からO(n3)へ改善できたことを示す.また,既存のSSReflectライブラリを用いたCoqの証明は,ほとんど書き換えることなく本研究のライブラリを用いた証明となる.例として,GonthierらのFeit-Thompson定理の約17万行におよぶ形式証明が,わずか10行以下の修正で,本研究のライブラリを用いた証明にできたことを示す.
著者
田中 恵海 高橋 謙輔 鳥海 不二夫 菅原 俊治
雑誌
情報処理学会論文誌数理モデル化と応用(TOM) (ISSN:18827780)
巻号頁・発行日
vol.3, no.1, pp.98-108, 2010-01-26

本研究では,日本の中学校の一学級を対象とし,教師のいじめ対策行動の効果を検討するためのエージェントシミュレーションモデルを,ソシオン理論とハイダーの認知的均衡理論に基づいて作成し,教師のいじめ対策行動の効果を検討した.いじめは昨今の学級形成の重要な問題となっているが,その対策は十分確立できていない.教師による学級内のいじめ対策方法を確立するためにはその効果を確認する必要があるが,そのためには長期にわたる観測を行う必要があるため,難しい.本研究では,教師および生徒をエージェントとし,エージェント間の対人関係形成の変異をコンピュータによるエージェントシミュレーションで再現し,その効果を推定する.本研究では対策行動として「班行動,出席停止,予防活動」の3つをモデル化し,それぞれに対していじめ被害者および加害者の割合,全生徒間の好感度平均,教師に対する全生徒の好感度平均から各いじめ対策行動の効果と影響を検討した.本実験から,学級におけるいじめ対策行動として最も適切である学級運営手法は「予防活動」であるとの示唆を得た.
著者
山崎 彰
出版者
山形大学歴史・地理・人類学研究会
雑誌
山形大学歴史・地理・人類学論集
巻号頁・発行日
no.3, pp.1-36, 2001-03-01

Keywords : Brandenburg, Gutsherr (schaft), adliger Amtstrager, Kriegskommissariat キーワード:ブランデンブルク, 農場領主(制), 官職貴族, 軍政コミサリアート
著者
森川 幾太郎 菊池 久人
出版者
山形大学
雑誌
山形大学紀要. 教育科学 = Bulletin of Yamagata University. Educational Science
巻号頁・発行日
vol.12, no.4, pp.13(381)-45(413), 2001-02-15

概要 : この論攷は,ニ部で構成され,その第一部を第一筆者が,第二部を第二筆者がそれぞれ担当する。第一部では,森川が過去において行った提案と対比しながら,D'AmbrosioやP.Gerdesらが提唱する民族数学の特徴を明らかにする。例えば,彼らは,図形や数に関わる話題をその教育素材として取り上げても,物理分野や量を主体にした算術分野の話題を取り上げていないことを述べる。第二部では,山形県内に現存する算額の問題を原問題に,生徒がその発展問題作りに取り組んだ実践の概要と生徒の作った問題のいくつかを紹介する。 こうした民族文化の伝統を生かした生徒主体の問題作りに関わる展開も「民族数学」の提案には見ることができない。 Summary : In the first part, we point out some characteristics things in the ethnomathematic; 1) We can see often the geometrical things in the papers written representational persons to the branch. It would mean that they analyzed the memorial things or heritages being seen in present times from mathematical points. And then, we know that many persons tried to present the themes as mathematics education by analyzing many traditional geometrical constructions from previous days whether they had the recognitions to the ethnomathematics or not. We had the papers to analyze the skills to construct the traditional Japanese constructions as mathematics in junior high school students, also without a recognition to the ethnomathematics. 2) We have not an experience to see the papers to analyze the phenomena often met in the each area; To analyze the phenomena, we need the some methods such as measuring the many quantities, drawing the graphs to them or finding the formulas. To measure the many quantities, we must prepare the tools.
著者
小松 和彦
出版者
国立歴史民俗博物館
雑誌
国立歴史民俗博物館研究報告 = Bulletin of the National Museum of Japanese History (ISSN:02867400)
巻号頁・発行日
vol.68, pp.115-136, 1996-03-29

死はさまざまなイメージで語られる。生者にとって,死の体験を語ることができない限り,死は外在的なものであり,他人の死を眺め,その死の体験を想像し,そのイメージを作り上げることによってしか死を表現することができない。物部の葬送儀礼では,まずそのイメージは「生」のカテゴリーの象徴的逆転として語り示される。日常における「右」の強調に対して「左」の強調,日常の作法に対するその逆転の作法,等々。そうした葬式の作法によって「死」のカテゴリーが形成され,そして,そうした「死」の記号は死の記号であるがために,死という出来事の回りに配置され,日常生活のなかに持ち込むことがタブーとされることになる。日本では,葬式にこうした「死」の記号が用いられるのは一般的なことに属するが,物部の葬式ではそれがかなり徹底しているといっていいだろう。物部の葬式は,死者の霊の「あの世」への追放と「あの世」での再生を期待したモチーフを強調した儀礼となっている。その典型的儀礼行為が,山伏の宿借りを拒絶する奇妙な儀礼的問答(山伏問答)であろう。死出の旅に発ったはずの死者の霊が立ち戻ってくるということを演劇化したこの儀礼は,亡くなったばかりの死者とは,あの世に行くのを好まずに現世に戻ってくるものなのだ,という観念を前提にしており,物部の人々の死を迎える気持ちや死後観を如実に伝えているといえる。物部の葬送儀礼では,西方浄土観が強調されている。しかし,それは葬送儀礼が仏教の影響を強く受けているためであって,それ以前は,古代の地下の冥界にもつながるような他界観を持っていたことが「みこ神」儀礼などからうかがうことができる。しかし,西方浄土観にせよ,地下他界観にせよ,そのイメージはきわめて素朴で,現世こそ楽園であるということを強調している。一種の異装習俗である「師走男に,正月女」の埋葬習俗は,調査資料も乏しく,まだほとんど解明されていない習俗である。ここでの「異装」は,怨霊の一種である「七人みさき」に引かれるのを避けるために,「女」ならば「七人みさき」の災いが発現するので「女」を「男」とみせかけて埋葬する,いわば「トリック」である。「異装」して埋葬するという奇妙な埋葬法に関心が向かいがちであるが,むしろ問題の核心は,なぜ正月という「時」に「女」が死ぬと「七人みさき」が発現するのか,という点にある。物部村に限ったことではないが,葬送儀礼に参加した人たちは儀礼的ケガレ,いいかえれば一種の日常生活からの隔離の状態に入る。物部では,これを「ブクがかかる」と称している。物部では,ブクと呼ばれるケガレは死,出産,婚礼の際に生じるという。いわゆる誕生・結婚・死の人生における大きな節目に当たり時にブクが生じるのである。この人生の節目に当たる儀礼で共食するとブクがかかるという。したがって,物部では,ブクは儀礼に参加した人々のカテゴリーを浮き上がらせる機能も帯びている。
著者
三小田 美稲子
出版者
国士舘大学体育学部附属体育研究所
雑誌
国士舘大学体育研究所報 = The annual reports of health physical education and sport science (ISSN:03892247)
巻号頁・発行日
vol.34, pp.15-22, 2016-03-31

The purposes of this paper were to examine the relationship between music and sports and to consider the effects of music through an analysis of the music used in sporting competitions. This paper has focused specifically on music used in figure skating. Pieces of music that were used by gold medalists since 2000 were identified and each piece’s main features were examined. How well the skater’s movement matched the music was also examined. The music that is often used in competition changes key and tempo. The music combines sections in a different key and with a different tempo. In addition, many pieces that are used in figure skating are ethnic/folk music and have a narrative. The characteristics of the music inspired skaters to choreograph their performance, and they chose music that best fit their personality and technical strengths. All of the skaters sought to portray the atmosphere and delicate movements that the music conveyed during their routines. The music greatly affected the skaters’ performance. In light of these findings, music is closely related to sports.
著者
楢﨑 洋一郎
雑誌
人間文化研究 (ISSN:13480308)
巻号頁・発行日
vol.13, pp.129-143, 2010-06-30

日本の指導要録・調査書の開示請求をめぐる議論に、アメリカ合衆国の「家族の教育上の権利およびプライヴァシーに関する法律」いわゆる「FERPA」が影響を与えた。本稿では、まず、FERPAについて解説を付し、次に、「教育記録」の定義と第三者開示が争点となったファルヴォ事件連邦最高裁判所判決(Owasso Independent School District No.I-11 v. Falvo(2002))の全訳を示した。最高裁判所判決の最大の意義は、学校で教員が用いる教育学的な根拠のある教育方法が、プライヴァシーの権利の概念から過度の制約を受けないように配慮したことである。近代以降の学校教育は集団で行われてきており、その教育学的な意義・効果にも十分留意せねばならない。
著者
LEE Jong-Wha WIE Dainn
出版者
GRIPS Policy Research Center
雑誌
GRIPS Discussion Papers
巻号頁・発行日
vol.16-25, 2016-12

This study analyzes how changes in overall wage inequality and gender-specific factors affected the gender wage gap in Chinese and Indian urban labor markets in the 1990s and 2000s. Analysis of micro data present that contrasting evolutionary patterns in gender wage gap emerged over the period, showing a widened wage gap in China but a dramatically reduced gap in India. In both countries, female workers’ increased skill levels contributed to reducing the gender wage gap. However, increases in observed prices of education and experience worked unfavorably for high-skilled women, counterbalancing their improvement in labor market qualifications. Decomposition analyses show that China’s widened gap was attributable to gender-specific factors such as deteriorated observable and unobservable labor market qualifications and increased discrimination, especially against low- and middle-skilled female workers. For India, gender-specific factors and relatively high wage gains of low- and middle-skilled workers reduced the male–female wage gap.
著者
鈴木 貢
雑誌
情報処理
巻号頁・発行日
vol.58, no.1, pp.68-68, 2016-12-15
著者
秋山 寛子 和田 昌昭 中山 雅哉 加藤 朗 砂原 秀樹
雑誌
情報処理学会論文誌 (ISSN:18827764)
巻号頁・発行日
vol.57, no.12, pp.2675-2681, 2016-12-15

プライバシ保護の観点から匿名化技術の重要度が高まっており,なかでもk-匿名化が活発に研究されている.k-匿名化のためのアルゴリズムとしてはMDAVやVMDAVなどが提案されているが,数値データの匿名化において,それらは情報損失の観点から必ずしも最良のものとはなっていない.本論文では,それらのアルゴリズムによって得られたデータの分割を,k-匿名性を保ったまま修正して情報損失を極小にする方法を提案する.またそれを実装して,いくつかのデータセットに適用し評価を行う.データ総数をkで割った余りが大きい場合の多くで,MDAVやVMDAVによる情報損失を提案アルゴリズムにより改善可能である.また,提案アルゴリズムは,データ総数によらず高速に実行可能である.
著者
糸井 良太 田中 美栄子
雑誌
情報処理学会論文誌数理モデル化と応用(TOM) (ISSN:18827780)
巻号頁・発行日
vol.6, no.1, pp.31-37, 2013-03-12

戦略の自動進化を取り入れた繰返し囚人のジレンマモデルにおいて,特に2進表現による1次元遺伝子配列の複写変異や分離変異を点変異と組み合わせることで遺伝子の長大化の効果を考察することを目的としたLindgrenモデルがあり,その結果として生き残りやすい戦略に共通した特徴のあることが指摘された.我々はこのモデルに依拠して長大な遺伝子配列が出現するまでシミュレーションを行った結果をもとに,長期間生存する遺伝子の配列パターンに共通する性質,遺伝子長32以下の範囲内で,長寿戦略の約60%が[1001 0*0* 0*0* 0001]という形の遺伝子に対応することを突き止め,さらにこの形の遺伝子の性質が1.自分から裏切らない(最右遺伝子が1=協力),2.裏切られたらすぐに報復する(4つ組の第3要素が0=裏切り),3.裏切りが続くと自分から協力行動を行う(最左遺伝子が1=協力)の3要素であることを見出した.このことは,Lindgrenの先行研究で報告されている[1**1 0*** 0*** *001]の遺伝子配列に比べて,より明確に長寿戦略の遺伝子構造を同定することができたといえる.これらの戦略は単純なしっぺ返し戦略より強く,多様な戦略との対戦に勝利した結果,長期間生存し続けることのできるロバストな戦略であるといえる.このような戦略の出現・生存に対する条件について考察する.