Challenge: Doing Arithmetic Omega Words in Prolog

[Jan Burse]

Hi,

But since modern Prolog systems have bignums, I guess it
would be a nice exercise to provide a library for omega
words as an arithmetic entity.

With using SWI-Prolog web interface, one could even provide
the library over the net, so that somebody does not need
to install the Prolog interpreter, but can directly fiddle
over the net.

I would give it a try as follows. Define a datatype:

% Omega = omega(Integer,Integer)

Then go on an implement predicates:

% omega_add(+Omega, +Omega, -Omega)
% omega_sub(+Omega, +Omege, -Omega)
% omega_mul(+Omega, +Omega, -Omega)
% omega_div(+Omega, +Omega, -Omega)
% omega_compare(-Result, +Omega, +Omega)

The following guy below says that div is difficult, he
even says 1/x is difficult, but I doubt:
http://www.maa.org/sites/default/files/pdf/upload_library/22/Polya/00494925.di020680.02p0417i.pdf

Just remember the pumping lemma, when doing it. I guess
div can relatively easy be defined. But I admit that it
might need a little bit more computation than the other
predicates.

Who will do it first?

Bye




Julio Di Egidio schrieb:
> On Thursday, June 18, 2015 at 4:48:30 PM UTC+2, Jan Burse wrote:
> <snip>
>> That omega words are not all infinite sequences is clear by
>> Gödel diagonalization. Omega words can be enumerated by
>> enumerating alfa and beta. Let <,> the map that maps NxN to
>> N. And p1 and p2 its projections. Then the omega words are
>> enumerated as follows:
>>
>> f_k = p1(k) p2(k)^w
>>
>> Now diagonalization says that this function is not enumerated:
>>
>> d(i) = r-1-f_i(i)
>>
>> Where r is the radix maximum, or in when dealing with omega
>> words we call this the alphabeth cardinality. Proof:
>>
>> Assume there where a k such that f_k = d. Then f_k and d
>> must be pointwise equal, i.e. forall j f_k(j) = d(j). But
>> we see that d(k) = r-1-f_k(k) <> f_k(k).
>>
>> Q.E.D.
>>
>> Bye
>>
>> Hint 1: In the diagonalization proof the property that f
>> was defined via omega words drops out. The diagonalization
>> doesn't care much about this.
>
> (Thanks for the nice post.) Let me try and object to the above: that omega words are all infinite sequences is rather clearly so by definition, and diagonalisation of standard lists rather just proves nothing re omega sequences. Strictly speaking, the argument is simply invalid.
>
> Julio
>

[Jan Burse]

Well maybe rather:

% Omega = omega(Integer,Integer,Integer)

The third integer the non fractional part, to cover
arbitrary positive magnitudes.

Jan Burse schrieb:

[Jan Burse]

Jan Burse schrieb:

> Well maybe rather:
>
> % Omega = omega(Integer,Integer,Integer)
>
> The third integer the non fractional part, to cover
> arbitrary positive magnitudes.

Well sorry, maybe even:

> % Omega = omega(Integer,Atom,Atom)

Otherwise we cannot deal with zeros in front of
the two parts of an omega word. Sorry, Sorry.

Bye

[Jan Burse]

Julio Di Egidio schrieb:
> The diagonalisation of a standard list of omega
> sequences is not an omega sequence, it is a
> standard sequence. (No-QED. E.g., as you know,
> "2+2=4 hence the moon is made of cheese" is an
> invalid argument, not an inconsistency in arithmetic.)

I don't use the terms "standard list" or "omega sequence".
I use the terms "omega word", which is an element from
a set, call this set Omega.

------------------------ Math ----------------------

And I showed different ways of enumerating this set of
Omega, leading to the diagonalization argument. The
set Omega is here:

Omega = { alfa beta^w | alfa is a finite word,
beta is a finite word }

This enumeration is already redundant, if we don't
care about arithmetic. There is both syntactic redundancy
not only arthmetic redundancy. These are the unnormalized
omega words, which are syntacticall unnormalized.

They also include cases where alfa can be shorted in
size when beta is rolled. And where beta can be shortened
when beta is unduplicated. For example:

0.1 11^w

The alfa word is '1', and the beta word is '11'.
The omega word is '1' '11'^w.

Is not normalized form is:

0.1^w

In the normalized form the alfa word is '', and the
beta word is '1'. The omega word is '' '1'^w. The
above normalization from 0.1 11^w to 0.1^w is
syntactical. Aritmetic normalization is when we for
example go from:

0.9^w

To:

1.0^w

We will need both in a library providing arithmetic.
In diagonalization we show that there is an infinite
sequence, namely a function f : N -> R, which is not
element of Omega. Thats all. Not very exciting.

------------------------ Prolog ----------------------

BTW: The Prolog program could include a normalization,
as follows:

omega_norm(X,Y) :- omega_add(X,0,Y).

But I guess a better idea is to implement omega_norm/2
directly, and change the signature of the predicates:

% Omega = omega(Integer,Atom,Atom)
% NormOmega a subset of Omega
% Those omega words that are syntactically normalized
% and arithmetically normalized.

Then go on an implement predicates:

% omega_norm(+Omega, -NormOmega)
% omega_add(+NormOmega, +NormOmega, -NormOmega)
% omega_sub(+NormOmega, +NormOmega, -NormOmega)
% omega_mul(+NormOmega, +NormOmega, -NormOmega)
% omega_div(+NormOmega, +NormOmega, -NormOmega)
% omega_compare(-Result, +NormOmega, +NormOmega)

But it could be also that the predicates are
a little bit agnostic, whether the input is really
normalized. So probably the following would also work:

% omega_add(+Omega, +Omega, -NormOmega)
% omega_sub(+Omega, +Omega, -NormOmega)
% omega_mul(+Omega, +Omega, -NormOmega)
% omega_div(+Omega, +Omega, -NormOmega)
% omega_compare(-Result, +Omega, +Omega)

But with the later interface, you are not allowed to
do the following short cut:

omega_add(0, O, O).

Since this would break the protocol, that omega_add
returns a normalized omega.

So there are a lot of pros and cons when designing
a library doing the stuff, to show that we can compute
with omega words. But the algorithm I gave for addition
in a previous post should work, as far as I know.

Maybe should produce an Isabelle/HOL verification or
somesuch. Well this is also a funny idea.

Bye