加治/輪講
をテンプレートにして作成
[
トップ
] [
新規
|
一覧
|
単語検索
|
最終更新
|
ヘルプ
|
ログイン
]
開始行:
[[加治/研究室関連]]
* Haskell [#m1bae978]
**型クラス [#t995538f]
-型を集めて、その振る舞いを定義したもの?
**インスタンス [#cf0e0b51]
-型クラスの制約を満たすために定義した型
*A.3.2 天井と床 [#af8506aa]
**問題 [#i374c78d]
Paul Simonの歌には、''One man's ceiling is another man's floor.(ある者にとっての天井は別のものにとっての床である''とある。
これは、ある者の床が別の者にとっての天井であることを含意するか?2つの制
約をAlloyで形式化し、1つめが2つめを含意するというアサーションを検査せよ。
もし、仮定が足りなかったせいで意味の通らない反例が出てきた場合、その仮定を新たな制約として付け加え、検査し直せ。
**試行1 基本的な制約の記述 [#w7f5eee7]
sig Platform {}
sig Man {ceiling, floor: Platform}
fact PaulSimon {all m: Man | some n: Man | Above [n,m]}
pred Above(m, n: Man) {m.floor = n.ceiling}
assert BelowToo {all m: Man | some n: Man | Above [m,n]}
check BelowToo for 2
***意味1 [#ob48a176]
-sig Platform {}
--床および天井の集合
-sig Man {ceiling, floor: Platform}
--Manという集合にPlatformへのceilingとfloorという関係があるよ
-fact PaulSimon {all m: Man | some n: Man | Above [n,m]}
--PaulSimonの歌の制約を定義(Manを満たす全てのmにおいて、some n: Man(Manを満たすあるnに対してAbove [n,m]が成立)が成立
-pred Above(m, n: Man) {m.floor = n.ceiling}
--Aboveに対する制約(Manのn, mに対しmにとって床は、nにとっては天井である)
-assert BelowToo {all m: Man | some n: Man | Above [m,n]}
--これが成り立つかどうか。
---BelowToo:全てのMan mに対するあるMan nはAbove [m,n]がなりたつか。
-check BelowToo for 2
--BelowTooの対象を2としてチェック
---反例がある→invalid
***実行結果1 (反例の出力)[#ubd44939]
#ref(try1_1.png);
-おや?何かがおかしいです
#ref(try1_2.png);
-floorはちゃんとできている
--Man1がPlatform0を「床」と呼び、Man0がPlatform1を「床」と呼んでいる
#ref(try1_3.png);
-ceilingにておかしい
--Man0が同じPlatform1を、「床」とも「天井」とも呼んでいる
**試行2 おかしいところを修正 [#n3fd881e]
-以下の制約を追記
pred Geometry {no m: Man | m.floor = m.ceiling}
assert BelowToo' {Geometry[] => all m: Man | some n: Man | Above [m,n]}
check BelowToo' for 2
***意味2 [#ue9e6090]
-pred Geometry {no m: Man | m.floor = m.ceiling}
--その人から見て床と天井が同じ人はいない
---床と天井が同じなわけないだろうという制約
-assert BelowToo' {Geometry[] => all m: Man | some n: Man | Above [m,n]}
--先ほどのアサートに、「Geometryならば」という制約を追加した
-check BelowToo' for 2
--対象を2としてチェックする
---反例は見つからなかった
***実行結果2 [#t5da6eaa]
-run Geometry for 2 Platform, exactly 2 Man
--2つのPlatformに対し、二人の人で実行してみる
#ref(try2_1.png);&br;
#ref(try2_2.png);&br;
#ref(try2_3.png);
-このスコープでは、重複がなくなり題意を満たしているように見える。
--でもあれぇ?何か違うかも♪
--せーの♪でもそーんなんじゃだーめ
--何がだめなの?
#ref(sonnnakoto.jpg);
--撫子だと思った?残念!前田さんでしたー!
**試行3 [#a91d8183]
check BelowToo' for 3
***意味3 [#m894c764]
-check BelowToo' for 3
--では対象を3として実行してみる
***実行結果3 [#efabffde]
#ref(try3_1.png);
-「ある人Aにとっての天井が、Bにとっての床である」の対応関係
#ref(try3_2.png);
-各自にとっての天井の対応
--重複している
#ref(try3_3.png);
-各自にとっての床の対応
--重複していない
**試行4 [#wba8d2c6]
pred NoSharing {no disj m,n: Man | m.floor = n.floor || m.ceiling = n.ceiling}
assert BelowToo'' {NoSharing[] => all m: Man | some n: Man | Above [m,n]}
check BelowToo'' for 6
run NoSharing for 6
check BelowToo'' for 10
***意味4 [#g610c972]
-pred NoSharing {no disj m,n: Man | m.floor = n.floor || m.ceiling = n.ceiling}
--今までは、m,nに対して区別がなかったが(同じである可能性もあった)、今回は異なる者として定義し、ある者の床は、別の人の床ではない、ある人の天井は別の人の天井に鳴らないように定義する。
-assert BelowToo'' {NoSharing[] => all m: Man | some n: Man | Above [m,n]}
--「NoSharingならば」という制約を追加した。
-check BelowToo'' for 6
--スコープを6にして実行
-run NoSharing for 6
--反例なし。有効である。
-check BelowToo'' for 10
--もっと増やす
-大丈夫だったー
*8.3 ガラーキン法と重み関数 [#w09ebe3b]
**概要 [#r545b0c1]
-これまでの計算は厳密解があるものとしての話だった。
-しかし、実際の有限要素法の解析において厳密解は存在しない。
-ただ、近似式(&texvc(y(x));)は作ることができる。
**近似式の作り方 [#y034a539]
***重み関数について [#f144516e]
-ルールに従い適切な関数を探し出すという方法を用いる
-そのルールのなかに、重み関数と未知数(&texvc(a_1);)とは密接な関係にある
--未知数の管理区域内において重み関数は有限
--管理区域外ではゼロ
***ヘルムホルツ方程式について [#ge2f30c2]
&texvc(y(x)=\frac{y(L)-y(0)}{L}x+y(0)+a_1\frac{x}{L}\left(1-\frac{x}{L}\right));----(8.38)
-構成
--&texvc(y(x)=(\alpha^2);がゼロの時の解&texvc()+a_1\times();関数&texvc());
---関数は未知数と密接な関係にある
---かつ管理区域外の領域ではゼロになっている
-結論
--未知数に掛け算されている関数関数&texvc(\frac{x}{L}\left(1-\frac{x}{L}\right));は、その未知数の重み関数の条件を満足していることになる。
---領域内にある=&texvc(a_1);は有限、そして0ではないから関数も有限な値になる。
**ガラーキン法 [#o7067ef2]
-このように、近似式の一部を重み関数として流用する方法をガラーキン法と呼ぶ。
-変分法的な観点からいえば、変分=重み関数なので、近似解群を作れば重み関数も作れたということになる。
*8.4 ノイマン型境界条件の場合 [#t1980e5c]
**8.4.1 近似式とノイマン型境界条件との関係 [#n0c041c2]
***概要 [#i91955b2]
-これまでは、ディリクレ型境界条件のみを扱ってきた。
-このセクションではノイマン型の境界条件について簡単に触れる
***境界条件について復習 [#k86200d1]
-ディリクレ型
--&texvc(u(0)=c);
--&texvc(u(L)=d);
--未知数が境界で固定される
-ノイマン型
--&texvc(\left.\frac{du}{dx}\right|_{x=0}=e);
--&texvc(\left.\frac{du}{dx}\right|_{x=L}=f);
--未知数の''勾配''が境界で固定される
-4章16ページ目
***ノイマン型境界とは [#t556493f]
-ノイマン型境界においては、&texvc(dy/dx);が境界値として与えられる
-ノイマン型境界条件を適用するには、対象オブジェクトの変形の仕方が左右対称である必要がある
***ノイマン型の境界条件 [#g6a14c28]
一般的にノイマン型の境界条件は、式8.39で与えられる
&texvc(q=\left.\frac{dy}{dx}\right|_{x=L});----(8.39)
-この式の場合は、&texvc(x=L);の境界がノイマン型の境界条件となっている
--つまり、&texvc(y(L));(?)は&texvc(q);の値によって変動することになる。
--および、&texvc(q);が一定でも、近似解(&texvc(y(x)=y_0(x)+\delta y(x));)の精度によっても&texvc(y(L));は変化する。
--よって、図8.5に示すように、ノイマン型の境界において&texvc(\delta y(L));はゼロにならない。
--つまり、&texvc(\alpha^2);を変化させたときの変分から考えても、ノイマン型の境界において&texvc(\delta y(L));がゼロにならないことになる。
***ノイマン型の境界値 [#d89692e2]
-近似解(&texvc(y(x));)の&texvc(x=L);での値は、
--&texvc(q=\left.\frac{dy}{dx}\right|_{x=L});----(8.40)
-厳密解は(&texvc(y_0(L));)のノイマン型のノイマン型の境界値
--&texvc(q=\left.\frac{dy_0}{dx}\right|_{x=L});----(8.41)
---近似解と全く同じになる
-近似解は&texvc(y(x)=y_0(x)+\delta y(x));なので、重み関数&texvc(\delta y(x);)の&texvc(x=L);での微分はqの値に関係なく、式8.42のようにゼロでなくてはならない。
--つまり、&texvc(x=L);での&texvc(d\phi_1/dx=0);ということになる
---&texvc(\left.\frac{d\delta y}{dx}\right|_{x=L}=0);----(8.42)
-これまでの説明をまとめると
--表8.3
---条件2について、以下に説明する
*ノイマン型境界条件用の形状関数 [#sc725279]
-表8.4
--第1行はx=Lで微分が0にならない
--第2行はx=Lで微分が0
-ノイマン型境界条件を満足させるためには第2行に示す重み関数が必要
--しかし、解析は十分よい精度を出しているので、2番目の条件は必用条件ではない。
**非ガラーキン法 [#rc2fec2b]
-第2行を重み関数とし、第1行を&texvc(u(x));の近似として使う方法を、非ガラーキン法という
*用語 [#zffb4560]
**スカラー [#la94960f]
量だけを持つ値
終了行:
[[加治/研究室関連]]
* Haskell [#m1bae978]
**型クラス [#t995538f]
-型を集めて、その振る舞いを定義したもの?
**インスタンス [#cf0e0b51]
-型クラスの制約を満たすために定義した型
*A.3.2 天井と床 [#af8506aa]
**問題 [#i374c78d]
Paul Simonの歌には、''One man's ceiling is another man's floor.(ある者にとっての天井は別のものにとっての床である''とある。
これは、ある者の床が別の者にとっての天井であることを含意するか?2つの制
約をAlloyで形式化し、1つめが2つめを含意するというアサーションを検査せよ。
もし、仮定が足りなかったせいで意味の通らない反例が出てきた場合、その仮定を新たな制約として付け加え、検査し直せ。
**試行1 基本的な制約の記述 [#w7f5eee7]
sig Platform {}
sig Man {ceiling, floor: Platform}
fact PaulSimon {all m: Man | some n: Man | Above [n,m]}
pred Above(m, n: Man) {m.floor = n.ceiling}
assert BelowToo {all m: Man | some n: Man | Above [m,n]}
check BelowToo for 2
***意味1 [#ob48a176]
-sig Platform {}
--床および天井の集合
-sig Man {ceiling, floor: Platform}
--Manという集合にPlatformへのceilingとfloorという関係があるよ
-fact PaulSimon {all m: Man | some n: Man | Above [n,m]}
--PaulSimonの歌の制約を定義(Manを満たす全てのmにおいて、some n: Man(Manを満たすあるnに対してAbove [n,m]が成立)が成立
-pred Above(m, n: Man) {m.floor = n.ceiling}
--Aboveに対する制約(Manのn, mに対しmにとって床は、nにとっては天井である)
-assert BelowToo {all m: Man | some n: Man | Above [m,n]}
--これが成り立つかどうか。
---BelowToo:全てのMan mに対するあるMan nはAbove [m,n]がなりたつか。
-check BelowToo for 2
--BelowTooの対象を2としてチェック
---反例がある→invalid
***実行結果1 (反例の出力)[#ubd44939]
#ref(try1_1.png);
-おや?何かがおかしいです
#ref(try1_2.png);
-floorはちゃんとできている
--Man1がPlatform0を「床」と呼び、Man0がPlatform1を「床」と呼んでいる
#ref(try1_3.png);
-ceilingにておかしい
--Man0が同じPlatform1を、「床」とも「天井」とも呼んでいる
**試行2 おかしいところを修正 [#n3fd881e]
-以下の制約を追記
pred Geometry {no m: Man | m.floor = m.ceiling}
assert BelowToo' {Geometry[] => all m: Man | some n: Man | Above [m,n]}
check BelowToo' for 2
***意味2 [#ue9e6090]
-pred Geometry {no m: Man | m.floor = m.ceiling}
--その人から見て床と天井が同じ人はいない
---床と天井が同じなわけないだろうという制約
-assert BelowToo' {Geometry[] => all m: Man | some n: Man | Above [m,n]}
--先ほどのアサートに、「Geometryならば」という制約を追加した
-check BelowToo' for 2
--対象を2としてチェックする
---反例は見つからなかった
***実行結果2 [#t5da6eaa]
-run Geometry for 2 Platform, exactly 2 Man
--2つのPlatformに対し、二人の人で実行してみる
#ref(try2_1.png);&br;
#ref(try2_2.png);&br;
#ref(try2_3.png);
-このスコープでは、重複がなくなり題意を満たしているように見える。
--でもあれぇ?何か違うかも♪
--せーの♪でもそーんなんじゃだーめ
--何がだめなの?
#ref(sonnnakoto.jpg);
--撫子だと思った?残念!前田さんでしたー!
**試行3 [#a91d8183]
check BelowToo' for 3
***意味3 [#m894c764]
-check BelowToo' for 3
--では対象を3として実行してみる
***実行結果3 [#efabffde]
#ref(try3_1.png);
-「ある人Aにとっての天井が、Bにとっての床である」の対応関係
#ref(try3_2.png);
-各自にとっての天井の対応
--重複している
#ref(try3_3.png);
-各自にとっての床の対応
--重複していない
**試行4 [#wba8d2c6]
pred NoSharing {no disj m,n: Man | m.floor = n.floor || m.ceiling = n.ceiling}
assert BelowToo'' {NoSharing[] => all m: Man | some n: Man | Above [m,n]}
check BelowToo'' for 6
run NoSharing for 6
check BelowToo'' for 10
***意味4 [#g610c972]
-pred NoSharing {no disj m,n: Man | m.floor = n.floor || m.ceiling = n.ceiling}
--今までは、m,nに対して区別がなかったが(同じである可能性もあった)、今回は異なる者として定義し、ある者の床は、別の人の床ではない、ある人の天井は別の人の天井に鳴らないように定義する。
-assert BelowToo'' {NoSharing[] => all m: Man | some n: Man | Above [m,n]}
--「NoSharingならば」という制約を追加した。
-check BelowToo'' for 6
--スコープを6にして実行
-run NoSharing for 6
--反例なし。有効である。
-check BelowToo'' for 10
--もっと増やす
-大丈夫だったー
*8.3 ガラーキン法と重み関数 [#w09ebe3b]
**概要 [#r545b0c1]
-これまでの計算は厳密解があるものとしての話だった。
-しかし、実際の有限要素法の解析において厳密解は存在しない。
-ただ、近似式(&texvc(y(x));)は作ることができる。
**近似式の作り方 [#y034a539]
***重み関数について [#f144516e]
-ルールに従い適切な関数を探し出すという方法を用いる
-そのルールのなかに、重み関数と未知数(&texvc(a_1);)とは密接な関係にある
--未知数の管理区域内において重み関数は有限
--管理区域外ではゼロ
***ヘルムホルツ方程式について [#ge2f30c2]
&texvc(y(x)=\frac{y(L)-y(0)}{L}x+y(0)+a_1\frac{x}{L}\left(1-\frac{x}{L}\right));----(8.38)
-構成
--&texvc(y(x)=(\alpha^2);がゼロの時の解&texvc()+a_1\times();関数&texvc());
---関数は未知数と密接な関係にある
---かつ管理区域外の領域ではゼロになっている
-結論
--未知数に掛け算されている関数関数&texvc(\frac{x}{L}\left(1-\frac{x}{L}\right));は、その未知数の重み関数の条件を満足していることになる。
---領域内にある=&texvc(a_1);は有限、そして0ではないから関数も有限な値になる。
**ガラーキン法 [#o7067ef2]
-このように、近似式の一部を重み関数として流用する方法をガラーキン法と呼ぶ。
-変分法的な観点からいえば、変分=重み関数なので、近似解群を作れば重み関数も作れたということになる。
*8.4 ノイマン型境界条件の場合 [#t1980e5c]
**8.4.1 近似式とノイマン型境界条件との関係 [#n0c041c2]
***概要 [#i91955b2]
-これまでは、ディリクレ型境界条件のみを扱ってきた。
-このセクションではノイマン型の境界条件について簡単に触れる
***境界条件について復習 [#k86200d1]
-ディリクレ型
--&texvc(u(0)=c);
--&texvc(u(L)=d);
--未知数が境界で固定される
-ノイマン型
--&texvc(\left.\frac{du}{dx}\right|_{x=0}=e);
--&texvc(\left.\frac{du}{dx}\right|_{x=L}=f);
--未知数の''勾配''が境界で固定される
-4章16ページ目
***ノイマン型境界とは [#t556493f]
-ノイマン型境界においては、&texvc(dy/dx);が境界値として与えられる
-ノイマン型境界条件を適用するには、対象オブジェクトの変形の仕方が左右対称である必要がある
***ノイマン型の境界条件 [#g6a14c28]
一般的にノイマン型の境界条件は、式8.39で与えられる
&texvc(q=\left.\frac{dy}{dx}\right|_{x=L});----(8.39)
-この式の場合は、&texvc(x=L);の境界がノイマン型の境界条件となっている
--つまり、&texvc(y(L));(?)は&texvc(q);の値によって変動することになる。
--および、&texvc(q);が一定でも、近似解(&texvc(y(x)=y_0(x)+\delta y(x));)の精度によっても&texvc(y(L));は変化する。
--よって、図8.5に示すように、ノイマン型の境界において&texvc(\delta y(L));はゼロにならない。
--つまり、&texvc(\alpha^2);を変化させたときの変分から考えても、ノイマン型の境界において&texvc(\delta y(L));がゼロにならないことになる。
***ノイマン型の境界値 [#d89692e2]
-近似解(&texvc(y(x));)の&texvc(x=L);での値は、
--&texvc(q=\left.\frac{dy}{dx}\right|_{x=L});----(8.40)
-厳密解は(&texvc(y_0(L));)のノイマン型のノイマン型の境界値
--&texvc(q=\left.\frac{dy_0}{dx}\right|_{x=L});----(8.41)
---近似解と全く同じになる
-近似解は&texvc(y(x)=y_0(x)+\delta y(x));なので、重み関数&texvc(\delta y(x);)の&texvc(x=L);での微分はqの値に関係なく、式8.42のようにゼロでなくてはならない。
--つまり、&texvc(x=L);での&texvc(d\phi_1/dx=0);ということになる
---&texvc(\left.\frac{d\delta y}{dx}\right|_{x=L}=0);----(8.42)
-これまでの説明をまとめると
--表8.3
---条件2について、以下に説明する
*ノイマン型境界条件用の形状関数 [#sc725279]
-表8.4
--第1行はx=Lで微分が0にならない
--第2行はx=Lで微分が0
-ノイマン型境界条件を満足させるためには第2行に示す重み関数が必要
--しかし、解析は十分よい精度を出しているので、2番目の条件は必用条件ではない。
**非ガラーキン法 [#rc2fec2b]
-第2行を重み関数とし、第1行を&texvc(u(x));の近似として使う方法を、非ガラーキン法という
*用語 [#zffb4560]
**スカラー [#la94960f]
量だけを持つ値
ページ名: