Expressibility of output equals input. Negative and positive results (Q1323378)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Expressibility of output equals input. Negative and positive results |
scientific article |
Statements
Expressibility of output equals input. Negative and positive results (English)
0 references
10 May 1994
0 references
We examine the common and seemingly simple specification that the output stream equals the input stream. We show that this is not in full generality expressible in first-order or temporal logic by an infinite set of sentences or a recursive specification, but requires certain extra assumptions, such as the existence of a clock or discrete input values. The main negative results are stated for first-order expressibility and have direct corollaries for inexpressibility in first-order temporal logic: output equals input with arbitrary delay is not expressible by a (perhaps infinite) theory (Theorems 2 and 3), even with a timestamp (Theorem 8), and is not expressible for an \(\omega\) timeline by a sentence, even with a timestamp (Theorem 10). Output equals input with constant delay cannot be expressed for \(\omega\) timeline by a sentence with extra unary predicates over the timeline. As an example of the positive results, we show output equals input can be expressed by a sentence in the language with a (weak) clock if the base model contains either an extra function (Theorem 14), or arithmetic (Theorem 15).
0 references
first-order logic
0 references
temporal logic
0 references
specification language
0 references