Extending the idea to cover modelling artefacts and automatic API

[enness]

An interesting twist would be to treat anonymous activity by
participants as a form of computing and provide a formal service API
to it. In simplistic terms, one could write a program that would
submit a problem and wait for a response. A response may come in
minutes or years but it must be a text in a formal language. An
interactive web page could be one way to access this API but it also
must be deployed as a form of a web-service. The advantage of such
approach is that it is open both to humans and software. That is, a
piece of software could generate problem submission and another piece
of software could be trying to find a mistake in an algorithm. It
should not be obviously detectable whether a party is a machine or a
human. I'll try to illustrate below why a software-based participant
may be not a bad idea.

My other suggestion is to extend the project scope and consider a
wider range of artefacts that may be investigated by projects
participants and, consequently, have a more general notion of what it
means to investigate an artefact. There must be a generic framework in
place extensible to cover specific subjects. One of such subjects is
the current idea of algorithm (program) correctness and performance.

The basic idea of the general framework is that a proposer submits a
problem using one of problem meta-models. A meta-model defines a
specific kind of problem (e.g., it is a C program, or ELF binary, or
pseudo code, or text in English) and the set of criteria used to
assess the problem: correctness (yes/no), counter-example (data file),
opinion (informal English text) and so on. A participant only looks at
problems they can understand, that is, problems with specific meta-
models. Meta-model must completely define the format of a problem
submission so that one use a mechanic rule to test whether a
submission is well-formed.

My interest is in the following. Two examples of simple and well-
defined problems are theorem and model. Theorems are self-contained
and difficult ones (or, at least, seemingly so) pop up from time to
time when one verifies the correctness of a something (e.g., in Z,
VDM, CSP, B, TLA, Larch, Rise, etc). At the same time, construction of
a formal proof of a large system is fairly slow-paced activity so it
makes sense to wait for a week to get a result on some theorem.
Theorems come in form that is easy to interpret by a machine. There
are plenty of automated provers and a participant could well be some
new theorem prover program. Models are not really unlike programs
except, perhaps, efficiency is not normally a concern.

[Arseniy Alekseyev]

This generalisation is a little bit too extreme for me to be able to
comment on it.
However, I had some thoughts in that direction myself.

I guess the following qualifies as one of meta-models you described. :)

I noticed that any programming challenge is a competition between a
program trying to prove (or rather trueify) a quantified boolean
formula, and another program trying to falsify it.

In general, a quantified boolean formula can be (or not?) reduced to
the form of:
forall u1. exists e1. forall u2. exists e2. ... f(u1,e1,u2,...)
The competition between participating problems will then proceed in
the following way:

- The falsifier program produces a value u1, for which, he thinks, the
further expression does not hold.
- The trueifier program takes u1 and produces e1, for which, he
thinks, the further expression holds.
- The falsifier takes u1 and e1 and produces u2, and so on, until all
the quantified variables has been assigned.
- Afterwards, the f function is evaluated by the judging system and
its value determines the winner.

However, for practical reasons (performance) it may be necessary to
write the formula in a different form, like this:
forall u1. checku1(u1) && !forall e1. checke1(u1,e1) && !forall u2.
checku2(u1,e1,u2). ... f(u1, e1, u2, ...)
(I have replaced "exists" with "!forall !" here so that the similarity
between the alternating quantifiers is more obvious)
This transformation will allow to terminate the trueifier/falsifier
message exchange early in case the judging system determines that one
of them has already lost.

I will provide some examples:

1. Standard programming problem in the form of QBF
forall test. testValid(test) && exists output. => outputCorrect(test, output)

Here the specification had to provide two functions: "testValid" and
"outputCorrect".
Specification falsifier is a testing framework (trying choosing a bad test)
Specification trueifier is a program submission (trying to satisfy
"outputCorrect" condition whatever test it is given)

2. An optimisation problem without a known solution:
forall test. testValid(test) && exists output. wellFormed(output) &&
!exists(output2). wellFormed(output2) && better(output2, output)

Here the specification only provides "testValid", "wellFormed", and
"better" functions, which is trivial.
The trueifier will be a normal solution to an optimisation problem.
The falsifier's job will be to provide a test data, wait for the
program output, and then to try and give a counter-example breaking
it.

3. Chess problems
A chess problem can be expressed in terms of QBF. Normally it will be
recursive, but I don't want to handle a recursive QBF case yet.

!exists w1. let statew1 = turn(initialState, w1) in isValid(statew1) &&
!exists b1. let stateb1 = turn(statew1, b1) in isValid(stateb1) &&
!exists w2. let statew2 = turn(stateb1, w2) in isValid(statew2) &&
!exists b2. let stateb2 = turn(statew2, b2) in isValid(stateb2) ...
(let it be 20 turns)

This formula, given the correct "turn", "initialState" and "isValid"
functions, will make the trueifier and falsifier play chess until one
of them is unable to make a valid move. Yes, this does not handle the
draw case. Can it be easily added?

This looked great to me at first, but in practice the time-out and
output overflow handling becomes a bit of a problem. For example, what
to do if a specification function times out? Or if a program is given
such an input for which the only possible correct output causes an
output overflow? One may say that such issues are specification
deficiencies, but the system will have to handle them and assign the
blame properly.

[Arseniy Alekseyev]

> forall test. testValid(test) && exists output.  => outputCorrect(test, output)

The "=>" is accidental of course.
It should be:

forall test. testValid(test) && exists output. outputCorrect(test, output)

[enness]

> In general, a quantified boolean formula can be (or not?) reduced to
> the form of:
> forall u1. exists e1. forall u2. exists e2. ... f(u1,e1,u2,...)

Sure, first order logic formula is reducible to either exists v . F(v)
or forall v. G(v) whichever you prefer where F and G are predicate
expressions. Do not even need a combination of quantifiers.

The problem of satisfying a formula is well-studied for predicate
logic (SAT solving) and for first order logic (SMT solving).
There are tools for these (z3, yices) and they hold competitions of
their own. So any step in this direction must differentiate from
these.

> The competition between participating problems will then proceed in
> the following way:
>
> - The falsifier program produces a value u1, for which, he thinks, the
> further expression does not hold.
> - The trueifier program takes u1 and produces e1, for which, he
> thinks, the further expression holds.
> - The falsifier takes u1 and e1 and produces u2, and so on, until all
> the quantified variables has been assigned.
> - Afterwards, the f function is evaluated by the judging system and
> its value determines the winner.

or just use game theory?

There are better notations for writing models (more humane to reader,
perhaps equivalent mathematically)
and the problem of state exploration is avoided by static analysis.
That's proving theorems about a program. It is, after all, the only
sure way to show that something posses a given property. For instance,
how you can show that QuickSort is a sorting algorithm without doing
some proofs?

Still, I would leave these complications behind for now. If there is
an API to submit a wide range of problems it could be used for a
number of interesting experiments. So my whole point is that the code
should be a faceless modular web-service where each module handles
certain kind of problems. Third-party developers should be able to
plug in their modules and thus cover new problem types.

[Arseniy Alekseyev]

> Do not even need a combination of quantifiers.

How come?
QBF is not reducible to polynomial-size SAT AFAIK.
How can you reduce the following without iteration over the a and b domains?
forall a. exists b. f(a,b)

In addition, as demonstrated, QBF carries some nice
human-understandable semantics, allowing to build almost natural
statements. This may be lost in a SAT conversion.

> my whole point is that the code
> should be a faceless modular web-service where each module handles
> certain kind of problems

That's a good idea. We should be keeping this in mind. However, I am
not convinced that the human web front-end should be using the web
API, but rather think that those could be just two different faces of
the same system.

[enness]

On Mar 21, 9:01 pm, Arseniy Alekseyev <arseniy.alekse...@gmail.com>
wrote:

> > Do not even need a combination of quantifiers.
>
> How come?
> QBF is not reducible to polynomial-size SAT AFAIK.
> How can you reduce the following without iteration over the a and b domains?
> forall a. exists b. f(a,b)
>
> In addition, as demonstrated, QBF carries some nice
> human-understandable semantics, allowing to build almost natural
> statements. This may be lost in a SAT conversion.

sure you right. I've got this mixed up with dnf

>
> > my whole point is that the code
> > should be a faceless modular web-service where each module handles
> > certain kind of problems
>
> That's a good idea. We should be keeping this in mind. However, I am
> not convinced that the human web front-end should be using the web
> API, but rather think that those could be just two different faces of
> the same system.

sure, web does not matter. My understanding is that once there is a
service, GUI is cleanly detached from the core logic.