In the process of cleaning-up my theorems for possible addition to set.mm I
found a fundamental inconsistency in the definition of my discrete time
operator ^. which is defined in terms of my continuous time operator @.
p@t says evaluate p at time t which is restricted to time the machine
starts operation, t=0, to the present instant, t=now, when the software
controlling the machine must decide what to do:
$( Define domain of time ` TIME ` from ` t = 0 ` to ` now ` $)
df-bl.time $a |- TIME = { x | ( x e. RR /\ 0 <_ x /\ x <_ now ) } $.
@ is used to declaratively specify machine timing behavior such as:
invariant
<< LRL: : --Lower Rate Limit
exists t~time --there was a moment
in (now-lrl)..now --within the previous LRL interval
that (n@t or p@t) >> --with a pace or non-refractory sense
which defines the fundamental effectiveness property of pacemakers treating
bradycardia. If the physician decides that the Lower Rate Limit should be
60 beats per minute, the LRL interval (lrl) will be 1 s. Then LRL asserts
that forever the pacemaker is operating, a heart beat will have occurred,
either intrinsically, n@t or paced p@t.
Naturally, ( p@t_1 ) @ t_2 <-> p@t_1.
Works great for threads with sporadic dispatch protocols. For periodic
threads, a discrete temporal operator shifts time of evaluation by an
integer number of thread periods.
p^-3 means the value of p, three periods before now. The discrete time
operator is defined in terms of the continuous time operator for which $d A
^. $. caused the error.
${
$d A ^. $.
$( Time Shift Value (for ` ^. ` not in ` A ` ) $)
df-bl.tsc $a |- ( ( A e. RR /\ B e. ZZ /\ D e. RR /\ ( now + ( D x. B ) )
e. TIME ) ->
( A ^. B ) = ( A @ ( now + ( D x. B ) ) ) ) $.
$}
This is to be applied only when no ^. are used to express A because
composition of ^. add the time shift values:
$( Distribute ` ^. ` over values $)
df-bl.tsdisc $a |- ( ( A e. RR /\ B e. ZZ /\ C e. ZZ ) ->
( ( A ^. B ) ^. C ) = ( A ^. ( B + C ) ) ) $.
If I am the only person using df-bl.tsc (or its wff equivalent df-bl.ts) I
can be sure to use them atomically . . . except all of the proofs of
distribution have the same problem.
The rigor of Metamath exposed a fundamental flaw in BLESS logic.
I'm considering removing ^. from the language entirely and try to prove the
periodic threads using only the continuous time operator.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/cf3b8654-0c1b-4b89-8f5e-63cfaa54a3f3n%40googlegroups.com.
