Home > Archive > Functional > June 2007 > (Semi)formally arguing referential transparency
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
(Semi)formally arguing referential transparency
|
|
| Joachim Durchholz 2007-06-05, 4:05 am |
| Hi all,
I asked this several months ago, but maybe I didn't phrase the question
well enough, so let me try again:
Assuming I have a read-only database.
More specifically, it's the table data is read-only; indexes may be
created or destroyed as the query optimizer sees fit.
It's clear that this design is referentially transparent as long as
there's no way to get at the current index configuration.
But how do I argue that from the sources?
Ideally, the arguments would be formal enough to be checkable by a
theorem verifier, though semi-formal reasoning would be enough for me to
work out the formal details.
However, I don't have the slightest idea how to even semi-formally argue
RT from sources.
Any ideas?
Regards,
Jo
| |
| Ville Oikarinen 2007-06-05, 4:05 am |
| On Tue, 5 Jun 2007, Joachim Durchholz wrote:
> Assuming I have a read-only database.
> More specifically, it's the table data is read-only; indexes may be
> created or destroyed as the query optimizer sees fit.
>
> It's clear that this design is referentially transparent as long as
> there's no way to get at the current index configuration.
>
> But how do I argue that from the sources?
By the lack of any delete, update and insert statements in your code?
- Ville Oikarinen
| |
| Joachim Durchholz 2007-06-05, 4:05 am |
| Ville Oikarinen schrieb:
> On Tue, 5 Jun 2007, Joachim Durchholz wrote:
>
>
> By the lack of any delete, update and insert statements in your code?
This would be arguing by specification.
I need to argue by source code.
Hmm... I'd have to demonstrate that any given call will always return
the same result, regardless of the configuration of the mutable data
used by the functions.
Seems that I answered myself.
Is there somewhere a list of lines of reasoning (aka. proof techniques)
that are useful for this kind of situation?
Regards,
Jo
| |
| Ville Oikarinen 2007-06-05, 4:05 am |
|
On Tue, 5 Jun 2007, Joachim Durchholz wrote:
>
> This would be arguing by specification.
> I need to argue by source code.
I was talking about source code. Of course we need to rely on the SQL
specification, too, unless you want to prove that the DBMS won't change
the data if you only use select statements. But I assumed you only want to
prove your own code RP.
- Ville Oikarinen
| |
| Aatu Koskensilta 2007-06-05, 4:05 am |
| On 2007-06-05, in comp.lang.functional, Joachim Durchholz wrote:
> Seems that I answered myself.
> Is there somewhere a list of lines of reasoning (aka. proof techniques)
> that are useful for this kind of situation?
Use induction. That is, define a suitable property P of the state of the
database, and show that it is preserved by the code that might be executed
between two queries (whether it's preserved locally, in between individual
steps in the code, is obviously not important) and that all states with
property P are observationally equivalent, i.e. for any query the result is
same no matter what the state of the database as long as P holds for the
state.
--
Aatu Koskensilta (aatu.koskensilta@xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
| |
| Joachim Durchholz 2007-06-05, 7:05 pm |
| Ville Oikarinen schrieb:
>
> On Tue, 5 Jun 2007, Joachim Durchholz wrote:
>
>
> I was talking about source code. Of course we need to rely on the SQL
> specification, too, unless you want to prove that the DBMS won't change
> the data if you only use select statements. But I assumed you only want to
> prove your own code RP.
Oh, sorry, I wasn't clear enough.
I meant the database implemented in the language itself. No external SQL
engine there.
Regards,
Jo
| |
| Joachim Durchholz 2007-06-05, 7:05 pm |
| Aatu Koskensilta schrieb:
> On 2007-06-05, in comp.lang.functional, Joachim Durchholz wrote:
>
> Use induction. That is, define a suitable property P of the state of the
> database, and show that it is preserved by the code that might be executed
> between two queries (whether it's preserved locally, in between individual
> steps in the code, is obviously not important) and that all states with
> property P are observationally equivalent, i.e. for any query the result is
> same no matter what the state of the database as long as P holds for the
> state.
Hmm... right, that could help.
P would simply be those invariants that are needed to guarantee that any
future functions that use the value will return the same results.
There are still a lot of practical obstacles, such as finding the
invariants, then proving/arguing that they are indeed enough to
establish identical results in the future. (Assuming that, for arbitrary
structures, such a proof would have to cover HOFs as well.)
But now I have something viable, and that's good enough. Somebody who
wants to write RT code that uses imperative stuff inside is allowed to
work hard for having that code accepted.
Thanks. I think I'm seeing much clearer now.
Regards,
Jo
| |
| Aatu Koskensilta 2007-06-06, 8:04 am |
| On 2007-06-05, in comp.lang.functional, Joachim Durchholz wrote:
> There are still a lot of practical obstacles, such as finding the
> invariants, then proving/arguing that they are indeed enough to
> establish identical results in the future. (Assuming that, for arbitrary
> structures, such a proof would have to cover HOFs as well.)
> But now I have something viable, and that's good enough. Somebody who
> wants to write RT code that uses imperative stuff inside is allowed to
> work hard for having that code accepted.
It is usually a non-trivial task to prove anything about real-world
programs -- even small real-world programs. It helps tremendously if the
program is written in a language with more-or-less mathematically defined
semantics.
--
Aatu Koskensilta (aatu.koskensilta@xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
| |
| Joachim Durchholz 2007-06-06, 10:09 pm |
| Aatu Koskensilta schrieb:
> On 2007-06-05, in comp.lang.functional, Joachim Durchholz wrote:
>
> It is usually a non-trivial task to prove anything about real-world
> programs -- even small real-world programs.
Some things are awfully difficult to prove, but others are surprisingly
easy.
For application code, the interesting properties are usually extremely
easy. (In an FPL, the code is often just a relatively straightforward
transcript of the specifications, so you don't do that much proving anyway.)
For library code, it depends: some properties are easy, most are so-so,
some are awful.
> It helps tremendously if the
> program is written in a language with more-or-less mathematically defined
> semantics.
I'd say it's best if most programs are RT by construction, but if an
inner loop turns out to be the bottleneck, it should be possible to
replace it with more efficient imperative code and prove that the result
is still RT.
In most cases, I'd think all you have to prove is that no mutable data
crosses the lexical scope of the function to prove that it's RT. The
tricky cases are when you need some kind of persistence across function
calls; things could very tricky indeed then. On the other hand, this
kind of situation arises in really heavy-duty library design, not in
everyday programming, nor in patching up a local bottleneck, so I don't
think that would be a problem.
Regards,
Jo
| |
|
|
|
|
|
|
|