λ-h.o.lのA.4がややこしかった。 厳密ではないかもしれないが以下のように考えてみた。
A.4 （Att Tt ∧ Att Ft）＝ ∀ ｘt Att ｘt
① ②
前提として ∀の定義が
∀ｘ At＝（λｘ At ＝ λｘ T） なので
∀ｘ Ａｔは、ＴかＦ
Ｔの場合は 定義より λｘ Ａｔが どんなｘでも→Ｔ
Ｆの場合は λｘ At と λｘ T が違うことがあるということなので
λｘ Atが どんなｘでも→Ｆ の場合と
ｘにより→Ｆだったり→Ｔだったり の場合がある
これを もとに Ａ．４を考えると
∀ ｘt Att ｘt は ＴかＦ
Ｔの場合は xt→Att xt が T→T＝AttTt ① F→T＝AttF ②
Fの場合は T→F ① F→F ② のときと
T→T ① F→F ② のときと
T→F ① F→T ② の３とおり考えられる
いずれの場合も A.４を満たす
※ A.４は 両辺とも Attの関数とみてもいいのでないかと、、、
ｆ：Ａtt→TまたはF つまりｆ（Att）＝T か Fになるという
イメージか。
放送大学で記号論理学の集中講義があったので学んでみた。
第６回以降は、タブローという証明支援ツールを実際に使って（サイト上にも自由に使えるアプリがあり非常に便利です）前提⊩結論 が正しいかどうか判定できます。機械的に変形していくだけで、結果がわかるというのが、なかなか素晴らしい！と思いました。
講義もとても丁寧なので、基本を理解するには書籍等で学習するよりスムーズです。
タブローを使っていると以前Coqを使ったのを思い出します。Coqより使いやすいようです。
記号論理学は、プログラミングの論理で混乱したときは、役立ちそうです。
Hom関手の理解が不十分と思い、再度復習してみた。
Cの対象Aに集合Hom（X,A）を対応させる
Cの射ｆ：A→Bに、「左からｆを合成」という関数を対応させる
Hom(X,f)=(f・) : Hom(X,A)→Hom(X,B)
これを 共変Hom関手といい Hom(X,-) :Ｃ→Ｓｅｔｓ と表す。
・Hom(X,-)という書き方は - → Hom(X,-) という関数（関手）ととらえるといいようだ。scalaの無名関数にもこの略記法がある。 A→Hom(X,A) f→Hom(X,f)の意味。
・射の合成関係をたもつことは、次のようにして確認できる。
g:A→Ｂ ｆ：Ｂ→Ｃ ｈ：Ｘ→Ａ として
Hom(X , f・g)(ｈ)＝(f・g)(ｈ)＝f・g・h
Hom(Ｘ,f)・Hom(X,g)(h)＝(f・)(g・)(ｈ)＝f・(g・ｈ)＝ｆ・ｇ・ｈ
∵ たとえば Hom(X,g)(h)の処理については
h=Hom(X,A）なので Hom(X,f)に適用すると、Hom(X,A)→Hom（X,B）だから、h=Hom(X,A）はHome（X,B）に変換される。つまり、Ｘ→Ｂで、これは、（ｇ・ｈ）を表している。この考え方を上記のすべての式変形に適用していく。
圏論学習会第８回のFokkingaの相互再帰定理を使ったsteep関数（例題）の実装を、Elmで確かめてみた。
T ← F（T）
<steep,sum> ↓ ↓
Bool×Int ← F（Bool×Int）
<[c,f],[d,g']>
<steep,sum>=(| <[c,f],[d,g']> |) ←Catgamorphism
※foldのイメージは、Listから一つずつaを取り出し、(b,s)のタプル つまり（Bool×Int）：steepとsumの結果のペアに、適用して畳み込んでいく（積み重ねていく）というイメージ
> c=(True,0)
(True,0) : ( Bool, number )
> fnx a (b,s) = ( a > s && b , a + s)
<function> : number -> ( Bool, number ) -> ( Bool, number )
> lst2=[32,16,8,4,2]
[32,16,8,4,2] : List number
> Tuple.first (List.foldr fnx c lst2)
True : Bool
> lst3=[32,16,8,4,4]
[32,16,8,4,4] : List number
> Tuple.first (List.foldr fnx c lst3)
False : Bool
foldも奥が深い。
