Pure specification language
Laurent Martelli
there does not exist two different programs that are equivalent.
If it does not exist, do you think that such a language can be
specified ?
The C programming language does not satisfy this definition since you
can do one thing in several ways.
An example of a language that satisfies the definition is a language
for specifying polynomial functions in which a valid program is a list
of real numbers; (1 5 2) would represent the polynom 1+5x²+2x³. But
this is not a "general purpose" language.
--
Laurent Martelli
mart...@iie.cnam.fr
Torkel Franzen
>I am wondering if there exists a general purpose language such that
>there does not exist two different programs that are equivalent.
No, since any effective enumeration of algorithms sufficient for
computing every computable function will contain equivalent
algorithms.
Michael David WINIKOFF
>I am wondering if there exists a general purpose language such that
>there does not exist two different programs that are equivalent.
Intuitively, no such language could be Turing complete.
If it was, you could check for termination by checking whether
the program was syntactically identical to the canonical non-terminating
program. The only way I can see to escape this argument is that the non-terminating
program be highly non-obvious ... in this case though the language is likely
to be highly unuseable: if you can't easily write an infinite loop you probably can't
write most things easily.
Looking at some examples, even simple grammars don't satisfy this condition.
(e.g. A -> aA | a vs. A -> aA | a | aA) although some normal forms for grammars
might satisfy the condition.
Michael
>--
>Laurent Martelli
>mart...@iie.cnam.fr
Laurent Martelli
Torkel> Laurent Martelli <mart...@iie.cnam.fr> writes:
>> I am wondering if there exists a general purpose language such
>> that there does not exist two different programs that are
>> equivalent.
Torkel> No, since any effective enumeration of algorithms
Torkel> sufficient for computing every computable function will
Torkel> contain equivalent algorithms.
In such a language, there would not exist two valid and different
programs representing the same algorithm.
So, your statement does not seem to answer the question.
--
Laurent Martelli
mart...@iie.cnam.fr
Nick Maclaren
In article <8108f9$qne$1...@mulga.cs.mu.OZ.AU>, wini...@cs.mu.oz.au (Michael David WINIKOFF) writes:
|> Laurent Martelli <mart...@iie.cnam.fr> writes:
|>
|> >I am wondering if there exists a general purpose language such that
|> >there does not exist two different programs that are equivalent.
|>
|> If it was, you could check for termination by checking whether
|> the program was syntactically identical to the canonical non-terminating
|> program. The only way I can see to escape this argument is that the non-terminating
|> program be highly non-obvious ... in this case though the language is likely
|> to be highly unuseable: if you can't easily write an infinite loop you probably can't
|> write most things easily.
Or relax the requirement to be only that there are no equivalent
but different terminating programs. There certainly ARE such
languages, but I believe that all are trivial. However, I can't
think of an obvious proof that this property is incompatible
with Turing completeness.
If you make a language more abstract, then you clearly can do it.
Take an arbitrary Turing complete language A, and create a language
A' such that the elements of A' are the equivalence classes of A.
Q.E.D.
Regards,
Nick Maclaren,
University of Cambridge Computing Service,
New Museums Site, Pembroke Street, Cambridge CB2 3QG, England.
Email: nm...@cam.ac.uk
Tel.: +44 1223 334761 Fax: +44 1223 334679
Laurent Martelli
Michael> Laurent Martelli <mart...@iie.cnam.fr> writes:
>> I am wondering if there exists a general purpose language such
>> that there does not exist two different programs that are
>> equivalent.
Michael> Intuitively, no such language could be Turing complete. If
Michael> it was, you could check for termination by checking whether
Michael> the program was syntactically identical to the canonical
Michael> non-terminating program.
You assume that there exists such a non-terminating program in the
language.
Most language allow to write infinite loops because they provide
"dirty" commands like "while" or "for".
Thinking about it, it's easy to write a non-terminating program in a
recursiver manner: (defun non-terminating () (non-terminating))
A solution would be to forbid such programs in the language. But it
would probably mean that the specification of the language is very
complicated, because it'd have to forbid all such non-terminating
programs. And there must be non trivial ones.
Michael> The only way I can see to escape this argument is that the
Michael> non-terminating program be highly non-obvious ... in this
Michael> case though the language is likely to be highly unuseable:
Michael> if you can't easily write an infinite loop you probably
Michael> can't write most things easily.
Michael> Looking at some examples, even simple grammars don't
Michael> satisfy this condition. (e.g. A -> aA | a vs. A -> aA | a
Michael> | aA) although some normal forms for grammars might satisfy
Michael> the condition.
I can't see the difference between "A -> aA | a" and "A -> aA | a | aA".
In fact the second grammar is redundant. Did you misspell something ?
--
Laurent Martelli
mart...@iie.cnam.fr
Henning Makholm
> Or relax the requirement to be only that there are no equivalent
> but different terminating programs. There certainly ARE such
> languages, but I believe that all are trivial. However, I can't
> think of an obvious proof that this property is incompatible
> with Turing completeness.
Roget's (sp?) theorem says that there is a compiling bijection between
any pair of acceptable enumerations. This means that, because there
are two different but equivalent terminating Turing machines, there
will be different but equivalent programs in any acceptable language.
There's a proof of the theorem in Neil D. Jones: Computability and
Complexity From A Programming Persprective. (My copy is at home, so I
can't give you the page reference).
One of the lemmas in that proof actually says in any acceptable
language, there are arbitrarily large (hence infinitely many)
programs that are equivalent to any given program.
--
Henning Makholm "*Jeg* tænker *strax* på kirkemødet i
Konstantinopel i 381 e.Chr. om det arianske kætteri..."
Torkel Franzen
> In such a language, there would not exist two valid and different
> programs representing the same algorithm.
I don't see what you mean. I'm saying that there will always be
equivalent algorithms, i.e. different programs computing the same
function, which I took to be the meaning of "equivalent programs".
Paul E. Black
> |> Laurent Martelli <mart...@iie.cnam.fr> writes:
> |>
> |> >I am wondering if there exists a general purpose language such that
> |> >there does not exist two different programs that are equivalent.
>
> If you make a language more abstract, then you clearly can do it.
> Take an arbitrary Turing complete language A, and create a language
> A' such that the elements of A' are the equivalence classes of A.
> Q.E.D.
Being a coding type, here's an argument that no (useful) general
purpose language exists.
Given a function f(n) which can be written in the language, one should
be able to write a function g(n) which is f(n)+3 (the 3 is an
arbitrary constant). One should be able to write a function h(n)
which is n-3. Now, if I can compose functions (programs) in any
reasonable way, I can write h(g(n)) which is f(n), written in what is
likely to be a different way.
One could argue that the language could simply not allow programs with
unsimplified expressions, to force the +3-3 to be removed. However
since one can make the encoding function, g(n), quite complex, it is
unclear if one could reasonably determine if no unsimplified
expressions remain. Thus checking for valid programs would be very
hard.
-paul-
--
Paul E. Black (p.b...@acm.org)
Laurent Martelli
Torkel> Laurent Martelli <mart...@iie.cnam.fr> writes:
>> In such a language, there would not exist two valid and different
>> programs representing the same algorithm.
Torkel> I don't see what you mean. I'm saying that there will
Torkel> always be equivalent algorithms, i.e. different programs
Torkel> computing the same function, which I took to be the meaning
Torkel> of "equivalent programs".
That's what I meant by "equivalent programs". But I wondered if there
exists a language which does not include such programs.
--
Laurent Martelli
mart...@iie.cnam.fr
Michael David WINIKOFF
>Or relax the requirement to be only that there are no equivalent
>but different terminating programs. There certainly ARE such
>languages, but I believe that all are trivial. However, I can't
>think of an obvious proof that this property is incompatible
>with Turing completeness.
What about programs that terminate sometimes, but not always?
I'm not certain this helps - you could probably construct programs
which terminated depending on difficult mathematical propositions then
test whether these propositions hold by comparing with terminating
programs with equivalent output behavior.
>If you make a language more abstract, then you clearly can do it.
>Take an arbitrary Turing complete language A, and create a language
>A' such that the elements of A' are the equivalence classes of A.
>Q.E.D.
This is effectively changing the meaning of "equivalent" to semantically
equivalent rather than syntactically equivalent (which I think is what
Laurent meant).
Michael
Michael David WINIKOFF
>You assume that there exists such a non-terminating program in the
>language.
Any language that's Turing complete must have ways of constructing
infinite loops. I've argued (informally) that if you want
(presumably syntatic) equivalence between programs you can't have
Turing completeness.
>A solution would be to forbid such programs in the language. But it
>would probably mean that the specification of the language is very
Not necessarily.
Primitive recursive functions guarantee termination, finite state
machines give termination, typed lambda calculus does
(assuming you don't have the Y combinator or recursive definitions).
> Michael> satisfy this condition. (e.g. A -> aA | a vs. A -> aA | a
> Michael> | aA) although some normal forms for grammars might satisfy
>I can't see the difference between "A -> aA | a" and "A -> aA | a | aA".
>In fact the second grammar is redundant. Did you misspell something ?
No, the point is that these two grammars are semantically identical
(they generate the same language) but they are syntactically different.
A simpler example is the two programs
x = x*2
and
x = x+x
which are semantically equivalent, but syntactically different.
Michael
Torkel Franzen
> That's what I meant by "equivalent programs". But I wondered if there
> exists a language which does not include such programs.
Right, and my answer was No.
Ariel Scolnicov
> [...]
> If you make a language more abstract, then you clearly can do it.
> Take an arbitrary Turing complete language A, and create a language
> A' such that the elements of A' are the equivalence classes of A.
> Q.E.D.
This is not was is usually thought of as "a language". It works
because what could be called "syntax checking", i.e. deciding if a
number is a valid encoding of a program, becomes non-recursive. For
instance, if you chose to encode A' by the code of A, the TM in [A']
with the smallest encoding (for some given TM encoding), it would be
non-recursive to check whether a given number is a valid encoding
(i.e. encodes for the smallest TM in its class).
You can build similarly "dishonest" encodings which solve the Halting
Problem. For instance, take your favourite encoding f(M), and define
a new encoding g: for a TM M which halts on null input, g(M)=2*f(M);
otherwise, g(M)=2*f(M)+1. Note that deciding halting for a TM encoded
by g is trivially recursive, except for the small matter that checking
input for correctness doesn't work.
Regarding the original question: it would seem Rice's theorem could
also be used to rule out any "unique" encoding of all recursive
function.
--
Ariel Scolnicov |"GCAAGAATTGAACTGTAG" |ari...@compugen.co.il
Compugen Ltd. |Tel: +972-2-6795059 (Jerusalem) \ 100% recycled bits!
72 Pinhas Rosen St. |Tel: +972-3-7658520 (Main office)`--------------------
Tel-Aviv 69512, ISRAEL |Fax: +972-3-7658555 http://3w.compugen.co.il/~ariels
Nick Maclaren
Ariel Scolnicov <ari...@compugen.co.il> wrote:
>nm...@cus.cam.ac.uk (Nick Maclaren) writes:
>
>> [...]
>> If you make a language more abstract, then you clearly can do it.
>> Take an arbitrary Turing complete language A, and create a language
>> A' such that the elements of A' are the equivalence classes of A.
>> Q.E.D.
>
>This is not was is usually thought of as "a language". It works
>because what could be called "syntax checking", i.e. deciding if a
>number is a valid encoding of a program, becomes non-recursive. For
>instance, if you chose to encode A' by the code of A, the TM in [A']
>with the smallest encoding (for some given TM encoding), it would be
>non-recursive to check whether a given number is a valid encoding
>(i.e. encodes for the smallest TM in its class).
Oh, yes. There are circumstances where working with such abstractions
are useful, but I can't think of any in this case.
A.P. Turnbull
>there does not exist two different programs that are equivalent.
>
>specified ?
The answer is no, if you want your language to be Turing complete (and
if you're thinking of C then you do), and yes otherwise.
A Turing complete machine can simulate a Turing machine (definition).
You can't always tell whether a Turing machine program will halt (the
halting problem is a standard theorem).
Our hypothesised simulation must therefore fail to halt if it
simulates some programs which fail to halt, since if it produced a
useful answer it would have solved the halting problem, and if it
produced an ambiguous answer it would not be a simulation. (This is a
bit wooly, but you can see how it could be tightened up - start by
defining simulation properly).
But then the halting problem applies to the language itself. We can't
tell if programs are equivalent to a non-halting program.
Therefore any Turing-complete language includes programs which are
equivalent but can't be proved so, and that means you can't eliminate
them.
---
To be more concrete, consider the following three programs (which can
all be written for a Turing machine):
1. answer = true
2. answer = false
3. answer = <insert favourite unsolved problem of mathematics>
Which two are equivalent?
Alistair