changeset 5:75a40129f638

*** empty log message ***
author kono
date Fri, 19 Jan 2001 04:25:07 +0900
parents 029b5a5ac494
children 9b86eb10b61c
files problems
diffstat 1 files changed, 36 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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
 
 えーと、