🚀 go-pugleaf

$@>.NSAo(J@$@N6C+Bg3X$G$9!#(J

In article <TANABE.93Mar10132850@Polaris.ai.cs.Fujitsu.Co.JP> tanabe@ai.cs.Fujitsu.Co.JP (Yoshinori TANABE) writes:

 |$@$4$V$5$?$7$F$$$^$9!%(J
 |
 |# $@$H8@$C$F$b3P$($F$$$i$C$7$c$i$J$$$+$bCN$l$^$;$s$,!$3XIt$N;~$K(J
 |# $@FqGH@h@8$N%<%_$G$*@$OC$K$J$j(J$@$^$7$?!%(J

$@$O$$!"3P$($F$$$^$9!#$*5W$7$V$j$G$9!#(J($@$3$N$"$$$5$D$r$3$NA0$N5-;v$G=q$$(J
$@$F$*$1$P$h$+$C$?$s$G$9(J$@$h$M!#(J)

 |$@EDJU(J> $@$H$$$&$N$,8m$j$G$3$3$GHsB8:_$,$o$+$k$N$O(J
 |$@EDJU(J>     $@=89gB2(J{b_r|r$@$O<B?t(J}$@$G!$(Jb_r={b_s|s$@$O(Jr$@$h$jBg$-$J<B?t(J}
 |$@EDJU(J>     $@$H$J$k$b$N(J
 |$@EDJU(J> $@$G$7$?!%!J:#EY$O9g$C$F$$$FM_$7$$$J$"!%!K(J
 |
 |$@>.NS(J> $@$$$$$(!"$3$&$$$&$N$bB8:_$7$^$9!#(J
 |
 |$@$3$l$O;d$NI=8=$,ITE,Ev$G$7$?!%(J``$@=89gB2(J{b_r|r$@$O<B?t(J}''$@$NI=8=(J
 |$@$G(J``$@0[$J$k(Jr$@$KBP$9$k(Jb_r$@$O0[$J$k(J''$@$3$H$rI=$7$?$D$b$j$K$J$C$F$$(J
 |$@$^$7$?!%$G$9$+$i!$(J

$@$"!"$=$&$$$&$3$H$@(J$@$C$?$s$G$9$+!#$=$l$J$i!"3N$+$K$*$C$7$c$kDL$j$G$9!#$9$J$o$A!"(J

 |  $@<B?tA4BN$N=89g$rDj5A0h$H$9$kC1<M(Jb$@$G(J$@!$A4$F$N<B?t(Jr$@$KBP$7$F(J
 |  b(r)={b(s)|s$@$O(Jr$@$h$jBg$-$J<B?t(J}$@$r$_$?$9$b$N(J $@$OB8:_$7$J$$!%(J
 |
 |$@$,@.$jN)$D$o(J$@$1$G$9$M!%(J

$@$H$$$&$N$O@5$7$$$G$9$M!#(J

 |$@>.NS(J> $@;d$,JL$N5-;v(J
 |$@>.NS(J> (Subject $@$,(J Situation Theory $@$K$J$C(J$@$F$k$d$D(J)$@$G>R2p$7$?(J
 |
 |$@$9$_$^$;$s!%$3$N5-;v$,8+Ev$?$i$J$$$N$G$9$,(J(fj.sci.math$@$G$9$h(J
 |$@$M!)(J)$@!$$b$7$h(J$@$m$7$+$C$?$i%a!<%k$G$G$bAw$C$FD:$1$^$;$s$+!)(J

$@$"$l!"FO$$$F$$$^$;$s$+(J? $@$3$l$OEDJU7/$N=j$@$1$J$N$+!"$=$l(J$@$H$b!"B>$N=j$K(J
$@$bFO$$$F$$$J$$$s$G$7$g$&$+$M$((J? $@$=$&$$$($P!"$A$C$H$b%U%)%m!<$,Mh$J$$$7!"(J
$@A4$/30$X=P$F$$(J$@$+$J$+$C$?$N$+$bCN$l$J$$$G$9$M!#(J($@$3$A$i$G$OFI$a$F$^$9!#(J)
$@$G$O!"%a!<%k$GAw$k$+!":FEj9F$9$k$+!"$I$A$i$+(J$@$K$7$?$$$H;W$$$^$9!#(J

 |$@>.NS(J> $@$b$A$m$s!"(JAFA $@$G$O!"(JCollapsing Lemma $@$H0c$C$F!"%0%i%U$,(J extensional $@$@(J
 |$@>.NS(J> $@$H$$$&2>Dj$rCV$+$J$$$N$G!"%0%i%U$,(J \in $@4X78$HF17?$K$J$k$H$O8B$i$J$$$o(J
 |$@>.NS(J> $@$1$G$9(J
 |
 |$@$3$3(J$@$,$A$g$C$H$o$+$j$^$;$s!%(J``extensional''$@$H$$$&$N$O(J
 |Collapsing Lemma $@$K=P$F$/$k$d$D!$$D$^$j!$%0%i%U(JG$@$G(J
 |(x$@$,(Jy$@$N;R@a$G$"$k$3$H$r(JxGy$@$H=q$/$3$H$K$7$F!$(J)
 |  [$@A4$F$N(JG$@$N@a(Jx$@$K$D$$$F(J [xGa <-> xGb]] -> a=b
 |$@$,(J$@@.$jN)$D$3$H$G$9$+!)$@$H$9$k$H!$(J

$@$"!"$3$l$O;d$N@bL@ITB-$G$7$?!#>/$7D9$/$J$j$^$9$,!"0J2<$K@bL@$7$^$9!#(J

$@7kO@$+$i8@$&$H!"(Jwell-founded $@$H$O8B$i$J$$0lHL$N%0%i%U$N>l9g!"(J
"extensional" $@$NDj5A$rJQ99$7$J$1$l$P$J(J$@$i$J$$$N$G$9!#JQ99$H8@$C$F$b!"(J
well-founded $@$J%0%i%U$K4X$7$F$O(J2$@$D$NDj5A$OF1CM$K$J$k$N$G!"$b$C$H$b$i$7(J
$@$$3HD%$@$H9M$($i$l$^$9!#(J

$@@bL@$NET9g>e!"$^$:!"%0%i%U$,(J2$@9`4X78(J G $@$GM?$($i$l$F$$$k;~!"(J3$@$D$NF1CM4X(J
$@78(J Eq1, Eq2, Eq3 $@$r0J2<$N$h$&$KDj5A$7$^$9!#(J

a Eq1 b := all x.(xGa <-> xGb)

Eq2, Eq3 $@$NDj5A$N=`Hw$H$7$F!"(J($@@a$N4V$N(J)2$@9`4X78(J P $@$r(J2$@9`4X78(J \Gamma P $@$K(J
$@$&$D$9$h$&$JBP1~(J \Gamma $@$r<!$N$h$&$KDj5A$7$^$9(J:

a (\Gamma P) b :=
    all xGa.exists yGb.(x P y) and all yGb.exists xGa.(x P y)

\Gamma $@$,:G>.$*$h$S:GBgITF0E@$r(J$@;}$D$3$H$O$9$0$K$o$+$j$^$9!#$=$3$G!"(J

Eq2 := \Gamma $@$N:G>.ITF0E@(J
Eq3 := \Gamma $@$N:GBgITF0E@(J

$@$HDj5A$7(J$@$^$9!#0lHL$K:G>.ITF0E@$K$h$kDj5A$r(J inductive definition $@$H$$$&(J
$@$N$O$h$/CN$i$l$F$$$kDL$j$G$9$,!":GBgIT(J$@F0E@$K$h$kDj5A$O(J coinductive
definition $@$H8F$P$l$F$$$F!"(Jnon-well-founded $@$JBP>]$r07$&;~$K$h$/=P$F$-(J
$@$^(J$@$9!#(J

$@$3$l$i(J3$@$D$K$D$$$F!"(JEq1 \subset Eq2 \subset Eq3 $@$O$9$0$o$+$j$^$9$,!"5U(J
$@8~$-$O0lHL$K$O$@$a$G$9!#(J

$@$5$F!"$3$l$i$NF1CM4X78$KBP1~$7$F!"(JG $@$,(J extensional $@$G$"$k$3$H$NDj5A$b0J2<$N(J
Ext1(G),Ext2(G),Ext3(G)$@$N(J3$@$D$,9M$($i$l$^$9(J:

Ext1(G):= all a,b.(a Eq1 b -> a = b)
Ext2(G):= all a,b.(a Eq2 b -> a = b)
Ext3(G):= all a,b.(a Eq3 b -> a = b)

Ext1(G) $@$,!"IaDL(J Collapsing Lemma $@$K=P$F$/$kDj5A$G$9$M!#$7$+$7!"$9$0$K(J
$@>ZL@$G$-$k$h$&$K(J Ext1(G) $@$H(J Ext2(G) $@$O0lCW$7$F$7$^$$$^$9!#$5$i$K!"(JG $@$,(J 
well-founded $@$J;~$K$O(J Ext2(G) $@$H(J Ext3(G) $@$b0lCW$9$k$N$G!"$I$NDj5A$r$H$C(J
$@$F$b9=$o$J$$$3$H$K$J$j$^$9!#$H$3$m$,!"0lHL$N%0%i%U(J G $@$KBP(J$@$7$F$O(J 
Ext2(G) $@$H(J Ext3(G) $@$O0lCW$7$J$/$F!"(JExt3(G) $@$N$[$&$NDj5A$r$H$i$J$$$H(J($@2f!9(J
$@$NL\E*$K$O(J)$@ITET9g$K$J(J$@$j$^$9!#$J$<$+$H8@$&$H!"Nc$($P!"@a(J a $@$h$j2<$NItJ,(J
(a $@$+$iJU$r?J$s$G9T$C$F$?$I$l$kItJ,!"(Ja $@$N?d0\JDJq$H(J$@$G$b$$$&$Y$-$b$N(J)$@$,(J

   a
   $@!&"*!&"*!&"*!&"*!&!D(J ($@L58B$KB3$/(J)

$@$N$h$&$K$J$C$F$$$F!"(Jb $@$h$j2<$NItJ,$b$^(J$@$?F1$87A$r$7$F$$$k;~!"(J
extensional $@$H$$$&>r7o$+$i(J a = b $@$,=P$F$[$7$$$N$G$9!#(Jnon-well-founded
sets $@$H$N(J$@4X78$r9M$($k$H$=$l$,<+A3$G$9$+$i!#$7$+$7!"(JExt2(G) $@$+$i$O(J a=b 
$@$,=P$^$;$s!#(JExt3(G) $@$+$i$O=P$^$9!#$3$N$h(J$@$&$K!"(Jnon-well-founded $@$J%0%i(J
$@%U$K$D$$$F$b!"(Ja $@$+$i2<$NItJ,$H(J b $@$+$i2<$NItJ,$,(J($@$"$?$+$b=89g$N$4$H$/$J(J
$@$,$a$?;~$K(J)"$@F1$87A(J"$@$r$7$F$$$k$J$i$P(J a = b $@$G$"$C$F$[$7$$$H9M$($k$H!"(J
Ext3(G) $@$r$b$C$F(J"extensional" $@$N(J$@Dj5A$H$7$?$[$&$,$h$$$H9M$($i$l$^$9!#(J

$@JdB-(J: coinductive definition $@$K$J$l$F$$$J$$J}!9$N$?$a$K!#(JEq3 $@$O(J$@!"MW$9(J
$@$k$K!"$9$Y$F$N(J a,b $@$K$D$$$F(J
  a P b -> all xGa.exists yGb.(x P y) and all yGb.exists xGa.(x P y)
$@$H$J$k$h$&$JF1CM4X78(J P $@$NCf$G:GBg$N$b$N$G$9!#$=$&$$$&F1CM4X78A4It$r(J 
union $@$7$?$b$N$@$H8@$C$F$b$$$$(J$@$G$9!#$"$^$j$o$+$j$d$9$/$J$C$F$J$$$+$bCN(J
$@$l$J$$$G$9$,!D!#$"$H!"(Jall xGa.$@!D(J $@$H$$$&5-K!$O$o$+$j$^$9$h$M!#(J
all x \in a.$@!D(J $@$H$$$&$N$HF1MM$G$9!#(J

$@$H$$$&$o$1$G!"(J

 |$@>.NS(J> $@$G!"<B?t$H$=$N>e$NBg>.4X78$r%0%i%U$H9M$((J$@$?;~!"$3$l$O(J extensional $@$G$J(J
 |$@>.NS(J> $@$$$N$G$9$,!"(J
 |
 |$@$H$N$3$H$G$9$,!$<B?t>e$NBg>.4X78$O(J extensional $@$K$J$k$H;W$$(J
 |$@$^$9$,!%(J

$@$b$&$*$o$+$j$H;W$$$^$9$,!">e$N(J Ext3(G) $@$N$h$&$K(J "extensional" $@$rDj5A$7(J
$@D>$;(J$@$P!"(Jextensional $@$G$J$/$J$j$^$9!#$^$?!"F1CM4X78(J Eq3 $@$G3d$C$?%0%i%U(J
$@$r:n$k$H!"(J1$@E@$@$1$+$i$J$kC1=c%k!<%W(J$@$N%0%i%U$K$D$V$l$^$9!#(J

 |$@$D$$$G$K!J$?$@$N46A[$J$s$G$9$,!K=q$$$A$c$$$^$9$H!$(J
 |
 |$@EDJU(J>   $@A4$F$NM-8~%0(J$@%i%U(JG$@$KBP$7$F(J*$@C1<M(J* f:node(G)->V $@$G!$(Jnode(G)$@$N(J
 |$@EDJU(J>   $@MWAG(Jx,y$@$KBP$7(J
 |$@EDJU(J>     x$@$,(Jy$@$N;R@a(J   iff   f(x) \in f(y)
 |$@EDJU(J>   $@$H$J$k$b$N$,B8:_$9$k!%(J
 |$@EDJU(J> $@$3$H$,>ZL@$G$-$k$h$&$G$9$M!%;d$O$3$l$GK~B-CW$7(J$@$^$7$?!%(J
 |
 |$@$H=q$$$?$N$G$9$,!$!VK~B-$7$?!W$H$$$&$N$O<B$O$A$g$C$H13$G$7$F!$(J
 |AFA$@$N!V$9$Y$F$NM-8~%0%i(J$@%U!W$r!V$9$Y$F$N(Jextensional$@$JM-8~%0%i(J
 |$@%U!W$K!$!V!A$J$k(Jd$@$,0l0U$KB8:_$9$k!W$r!V!A$J$kC1<M(Jd$@$,0l0U$KB8(J
 |$@:_$9$k!W$K$=$l$>$lJQ$($?$b$N$NJ}$,0u>]E*$J$N$K$J$"!%$H;W$$$^(J
 |$@$7$?!%(J

 |$@L5L7=b$K$J$k$N$+$b$o$+$i$J(J$@$$$7!$$J$C$?$H$7$F$3$&JQ$($k$H1~MQ(J
 |$@>e$&$^$/$J$$$N$+$b$7$l$J$$$G$9$1$I!%(J

"extensional" $@$NDj5A$r>e$N(J$@$h$&$KJQ$($l$P!"8xM}$r$3$&JQ$($F$bF1$8$@$H;W(J
$@$$$^$9!#$G$b!"1~MQ>e$O85$N7A$N$[$&$,JXMx$G$7$g$&$M!#$$$A(J$@$$$A(J 
extensional $@$J%0%i%U$K$D$V$5$J$/$F$b$$$$$N$G!#(J
--
			$@N6C+Bg3XM}9)3XIt?tM}>pJs3X2J(J    $@>.NS(J  $@Ao(J
			satoshi@whale.ryukoku.ac.jp
			0775-43-7523($@3X2J;vL3<<(J) 0775-43-7528($@8&5f<<(J)
			0775-43-7524(FAX)