# HG changeset patch
# User kono
# Date 979845907 -32400
# Node ID 75a40129f638f4b5ed9384197451aae86744a39f
# Parent  029b5a5ac4943f8e0faf47a2515793454bbbc6aa
*** empty log message ***

diff -r 029b5a5ac494 -r 75a40129f638 problems
--- a/problems	Fri Jan 19 02:03:27 2001 +0900
+++ b/problems	Fri Jan 19 04:25:07 2001 +0900
@@ -1,3 +1,23 @@
+
+Fri Jan 19 02:18:39 JST 2001
+
+<>empty と infinite = (true & false ) は、両立しない。
+<>empty = finite & empty = ~(true & false) & empty
+
+~(true & false ) はなにを示しているかと言うと...
+いつでも「終れる」ということ。infinite は、「終れない」
+
+ω区間には、empty exit は存在できない。正確には、
+    ... [ no-empty loop ] ....
+ということ。そういうsub 区間があれば良い。
+
+[](more) は? もちろん、これは、Lite では、false.
+     ~(finite & ~more)
+     ~(~(true & false) & ~more))
+     ~(~(true & false) & empty))
+これが ω区間で true になるためには...
+
+[]のinifinite versionは?
 
 http://research.commpaq.com/SRC/esc/
 
@@ -20,6 +40,22 @@
    <>empty がfalse
 どうも正しそうだな。
 
+えーと、何か、安全なアルゴリズムがありそうだけど...
+簡単なのは、すべてのループをdepth first で探すことだな。
+
+とすると、finitarity をチェックするのは結構面倒になる。
+
+finitarity とはなに?
+    ループには必ずtrue exitがある
+infiniteness とは、
+    exit のないループがある
+
+[]<>(p) = <>[](p) は、どうなるんだろう?
+   <>(p) = finite & p
+   ~(finite & ~(finite  & p)) = finite & ~(finite & ~p)
+ですか。
+
+
 Fri Jan 19 00:33:43 JST 2001
 
 えーと、