]>
Lambda the Ultimate - Comments
http://lambda-the-ultimate.org
CommentsenNow with encodings
http://lambda-the-ultimate.org/node/5425#comment-94196
<p>The question I think has become whether there is a difference between running L<sup>w</sup>(
C<sup>w</sup>(A<sup>w</sup>), x) and running L<sup>w</sup>( C<sup>w</sup>(A<sup>k</sup>), z). But that's not exact, because within the
world w, we do not know what is happening outside, how those objescts are being
used. What we can be certain of is that those objects must somehow exist - that, wathever happens outside, it will have all the information that is
assumed within L<sup>w</sup>, C<sup>w</sup>, and A<sup>w</sup> or A<sup>k</sup> at its disposal.
<p>So now the question becomes that of finding a path to undecidabity with L<sup>w</sup>, C<sup>w</sup>, A<sup>w</sup>,
and x, that is unavailable to L<sup>w</sup>, C<sup>w</sup>, A<sup>k</sup> and z, and that is shorter than any available
to the later.
<p>So let's examine the following path.
<p>We have L<sup>w</sup>, C<sup>w</sup>, C<sup>w</sup>(A<sup>w</sup>), and x . We analyze C<sup>w</sup>(A<sup>w</sup>) and see that it contains
L<sup>w</sup> and an enumeration of C<sup>w</sup> encoded machines and inputs. We learn that we must
use those enumerations to find out the next necessary operation, which is
specified in the diagonal row to the x column. We find out what is in that row,
and find C<sup>w</sup>(A<sup>w</sup>). We already have C<sup>w</sup>(A<sup>w</sup>), so we can recognize it. And now we
learn that we have to output the contrary; but we already know that the
contrary must be the same, we have already identified both machines as the
same. Here we reach an undecidable state.
<p>We have L<sup>w</sup>, C<sup>w</sup>, C<sup>w</sup>(A<sup>k</sup>), and z . We analyze C<sup>w</sup>(A<sup>k</sup>) and see that it contains
L<sup>k</sup> and an enumeration of C<sup>k</sup> encoded machines and inputs. We learn that we must
use those enumerations to find out the next necessary operation, which is
specified in the diagonal row to the z column. We find out what is in that row,
and find C<sup>k</sup>(A<sup>k</sup>). We already have C<sup>w</sup>(A<sup>k</sup>), <strong>**but**</strong> we cannot recognize it; as of
now, we do not understand the k encoding. Now we have to use L<sup>k</sup> to analyze A<sup>k</sup>
and understand what to do. We are already past the state where we found
undecidability in the previous case.
<p>So at the moment it semms to me that there is a path, the possibility of leaking seems real.
<p>[<em>edited a bit to remove redundancy</em>]
Thu, 27 Apr 2017 21:34:43 +0000Enrique Perez ArnaudA refutation of Gödel's first incompleteness theoremFor completeness
http://lambda-the-ultimate.org/node/5425#comment-94195
<blockquote>
making the world run Lw( Ak, z) for all possible k
</blockquote>
For all possible k and z. In this scheme, we should obtain undecidabiity (inconsistencies in the outputs) with one input z for each A, the input that corresponds to the diagonal cell in its own table.
And now, once we have appropriate pairs of undecidable (A<sup>k</sup>, z), we can question whether we can trace the A machines and distinguish A<sup>w</sup>.Wed, 26 Apr 2017 17:07:24 +0000Enrique Perez ArnaudA refutation of Gödel's first incompleteness theoremCategory collapses for another reason
http://lambda-the-ultimate.org/node/4964#comment-94194
Whoops, I wasn't attending the conversation very well while I was writing that. Jaques Carette shows me there's <a href="https://mathoverflow.net/questions/100158/negative-objects-in-categories">another known source of inconsistency in this system</a>, so there go my naive ideas about these types playing along well with "alien" types. Hmm.Wed, 26 Apr 2017 16:36:34 +0000Ross AngleThe Two Dualities of Computation: Negative and Fractional TypesBelated correction, and taming the frays of this system
http://lambda-the-ultimate.org/node/4964#comment-94193
Someone brought up this comment to me again, so I reread it.
First, I noticed a mistake I made:
<blockquote>In order to use <code>(/(1 + -Int))</code> as a list of Int via the isomorphism I gave, we have to prove <code>Int</code> isn't isomorphic to <code>-1</code>.</blockquote>
We would actually have to prove <code>Int</code> isn't isomorphic to <code>1</code>, not <code>-1</code>. So I suppose <code>(/(1 + -BNat))</code> is a fine type, isomorphic to <code>(/2)</code>. ^_^
Anyway, I want to say I didn't remember of my comments here as being a rebuttal of the type system. I think people had some inaccurate expectations of what the type system could do that I wanted to correct, and I found it interesting to explore corner cases I thought were interesting to explore, since the operational semantics can sometimes be a source of ideas for improving the type system design.
The operational semantics in the paper doesn't care if we divide by zero or put in types of infinite information content (like natural numbers or lists), even though these things don't correspond to the rational number axioms as well as the rest of the system does. While I thought these were details worth exploring, I think people would probably want to avoid these things in a practical use of the system. They clash with the rational number and information conservation metaphors, so they can produce a lot of conclusions.
If we simply set limitations on <code>0 <-> (-a + a)</code> and <code>1 <-> (/a * a)</code> that <code>a</code> must be a finite-depth structure composed of a few known type constructors, then I think that's enough to tame the behavior of this system in the face of infinities like <code>(mu a. 1 + a)</code> where the rational number laws don't apply.
With that restriction in place, I think these types could even be integrated into another type system. Alien types like <code>(a -> b)</code> would not be considered "finite" enough to use under <code>0 <-> (-a + a)</code> and <code>1 <-> (/a * a)</code> until there was a good reason to believe they were safe (e.g. a full implementation of values of type <code>(-(a -> b))</code> and/or <code>(/(a -> b))</code>).
Some type systems can already forbid division by zero, but I think the worst that would happen to other type systems is that we'd lose progress, just like we do with a language that has general recursion. My division-by-0 example used the isomorphism <code>0 <-> (0 * b)</code>, which introduces a logic variable of type <code>b</code> which has no constraints applied to it and never will. Any client waiting for a particular value of type code>b</code> won't make progress.
So, I'm very sorry if I made it out that this type system is nonsensical. Sometimes I can be all over the place in my exploration of trivialities, and it took me a while to figure out the benefits of this type system myself too. But I don't think I've seen any other system which has such a strongly typed treatment of backtracking and logic variables, and the isomorphism to rational numbers isn't easy to forget. I hear there's been a bit more work going on since this paper, so I want to check that out when I can.Wed, 26 Apr 2017 16:17:00 +0000Ross AngleThe Two Dualities of Computation: Negative and Fractional TypesLiving in an encoded world
http://lambda-the-ultimate.org/node/5425#comment-94192
<blockquote>
I suggest that the undecidability reasoning using A<sup>k</sup> is inherently reasoning about the place of A<sup>k</sup> in its own table
</blockquote>
<p>Agreed that the argument is inherently about A's own table. But that is not
incompatible with there being other cells in the table that correspond to other
A machines, cells that must be undecidable, but where undecidability will only be
met when we reach reasoning about them in their own tables.
<p>And what is in those cells is, basically, L<sup>j</sup> (A<sup>j</sup>, x) for A<sup>j</sup> in its own table, and L<sup>k</sup> (A<sup>j</sup>, x) for the same machine in other tables.
<blockquote>
<blockquote>
But now, with the non diagonal cell A<sup>k</sup>,z in the j table, your undecidable procedure will not work - immediately. It will have to descend to the k table to meet undecidability.
</blockquote>
I'm suggesting that this descent isn't anything new, but is how the procedure always worked;
</blockquote>
<p>Ok, so you agree that there may be a difference there. [<em>edited to add: you haven't really agreed, have you ;)</em>]
<p>The problem is that, if there is such a difference, it may leak the encoding to
the encoded.
<p>Suppose we are encoded and live in an encoded world. Let's call this encoding
w. Can we work out w from within? Of course not, we shouldn't be able to do
that. The encoding shouldn't leak to the encoded objeccts. But now imagine the following procedure.
<p>First, note that in this w world, running a Turing machine f is
effectively just doing L<sup>w</sup> ( f ).
<p>So we can concoct some enumeration of encodings, or of L machines, and use it to build an A
machine for each encoding, and run them. Since we are within w, what we are actually doing is
making the world run
L<sup>w</sup>( A<sup>k</sup>, z) for all possible k <strong><sup>*</sup></strong>. Now, should we be able to notice any difference between
running L<sup>w</sup> (A<sup>w</sup>, z), and running any other L<sup>w</sup> (A<sup>k</sup>, x)? Beacuse these are the 2
things we have agreed that may be different.
<p>If the above difference is correct and noticeable, we might be able to, among all A machines, identify A<sup>w</sup> as
the one that contains the w encoding, the encoding of our world.
<p>Note that I'm not saying saying that it must be noticeable and thus we must be
able to find w. All I say is that L<sup>w</sup> (A<sup>w</sup>, z) contains all
the information needeed to "fail" earlier than L<sup>w</sup> (A<sup>k</sup>,
x). So that whether it is noticeable and we do notice, may depend on the algorithm the L<sup>w</sup>
follow, which is outside of our control. However, it may also depend on A, which
is under our control, and we might be able to tweak A to expose the difference.
<p><strong>*</strong> [<em>edited to add: and z, see next comment</em>]Wed, 26 Apr 2017 15:24:35 +0000Enrique Perez ArnaudA refutation of Gödel's first incompleteness theoremEveryone's mad except me and thee...
http://lambda-the-ultimate.org/node/5425#comment-94191
I'm going to make a suggestion. I'm not 100% sure of it; I'd need to go back to my blog post and reread that part with this suggestion in mind, to see whether it fits; but I'm going to put the suggestion out here now, rather than wait to check it first and risk losing track of it before getting to the check.
I suggest that the undecidability reasoning using A<sup>k</sup> is inherently reasoning about the place of A<sup>k</sup> <i>in its own table</i>, the table that A<sup>k</sup> defines. That is, when you say
<blockquote>
But now, with the non diagonal cell A<sup>k</sup>,z in the j table, your undecidable procedure will not work - immediately. It will have to descend to the k table to meet undecidability.
</blockquote>
I'm suggesting that this descent isn't anything new, but is how the procedure always worked; it just wasn't obvious because we weren't considering multiple encodings.Wed, 26 Apr 2017 02:52:43 +0000John ShuttA refutation of Gödel's first incompleteness theoremAlmost seeking therapy
http://lambda-the-ultimate.org/node/5425#comment-94190
<p>I really think that I see and understand what you mean.
The only thing I'm not sure about is your suspicion of my intuition of the
problem. I think it is not correct, but I'm not 100% sure, and I'd hate to
repeat understood things when you already have shown me wrong. But since I'm
not sure, I'll risk it and try to detail how I see the problem in
light of what I think your suspicion is.
<blockquote>
And A doesn't need to know which row it occupies either.
</blockquote>
<p>Agreed
<blockquote>
the diagonal is actually defined by its hardcoding into the algorithm of A — even more specifically, it's defined by its hardcoding into the algorithm of Ai. So each Ai has its own diagonal that it implements.
</blockquote>
<p>Also agreed.
<p>Let's suppose we have 2 different encodings, and an enumeration of Turing
machines and inputs for each encoding, so that together they determine 2
different tables <strong>*</strong>, j and k. We can use them to build 2 A machines, A<sup>j</sup> and
A<sup>k</sup>. Let's also take that the machine A<sup>j</sup>, in its diagonal cell in the j table,
corresponds to the x input, and that the A<sup>k</sup> machine in the k table corresponds
to input z in the diagonal.
<p>Let's now limit our attention to the j table. What to put in the A<sup>j</sup>,x cell?
This cell corresponds to the n,n cell in your post, and the procedure will
result in the undecidability you describe.
<p>Now, in the <strong>same</strong> j table, there is also a row for A<sup>k</sup>, and also a column for the z
input. That row and column will not correspond -most probably- to a diagonal
cell. But we can check anyway what should be in the cell - and it should be
exactly the same as in the diagonal cell in the k table. This we have already
agreed, I think.
<p>But now, with the non diagonal cell A<sup>k</sup>,z in the j table, your undecidable
procedure will not work - immediately. It will have to descend to the k table
to meet undecidability. Your explanation leading to undecidability would not be identical to the one for
n,n - it would be a little bit longer.
<p>Is it a difference, or do I definitely seek therapy? ;) <strong>**</strong>
<p>What an agent -machine or otherwise- must (or may) do to fill in the A<sup>j</sup>,x cell in the j-table and find
undecidability is different than what it must do for the A<sup>k</sup>,z cell in the
same table. Your undecidable process in both cells differs.
<p>If the difference is real, I am despairing of being able to isolate it. Oracles
don't seem such a good idea, since using an oracle to build itself seems too
circular. Perhaps debugging, tracing the steps?
<p><strong>*</strong> [<em>edited to add: I am not supposing that the tables are filled finished tables or anything. Just that an L machine, and an enumeration of Turing machines in the encoding required by the L machine, determines a table. Any machine that has those hardcoded has access to the table - can work out the content of any cell.</em>]
<p><strong>**</strong>[<em>edited to add: Honest question. (Not the one about therapy, that's what the ;) if for.) From the clarity and cockyness of the first days of this discussion, I've come to, for the last couple of days, being continuously changing between: There is a difference. But it is insignificant. No, it is significant. Woah. No, but there is no difference. Oops, there is a difference, isn't there? </em>]Tue, 25 Apr 2017 18:17:31 +0000Enrique Perez ArnaudA refutation of Gödel's first incompleteness theoremdiagonal
http://lambda-the-ultimate.org/node/5425#comment-94189
I suspect there's a bottomless pit of technicalities one could get tangled up in with all these conversions between encodings; but, we seem to be getting past that to the essential concepts involved, which is where we want to be.
The diagonal in the table is defined by the way we enumerate the input strings (the column indices) and the way we enumerate the machine encodings (the row indices). Those choices are built in to machine A; machine A defines for itself what is the diagonal. We need the diagonal to cross-cut every row of the table, which is to say that we need A to cross-cut every row of the table, and behave in a way that demonstrates a problem with our supposition when it cross-cuts its own row. We don't have to know just when it cross-cuts its own row, which is to say, we don't need to know which row it occupies, exactly <i>because</i> it cross-cuts every row; that's the essence of the diagonalization method. And A doesn't need to know which row it occupies either. My head hurts just thinking about whether or not it's possible to guarantee that A knows its own row number; if it is possible to show that this cannot be guaranteed, there's probably a proof of it using... diagonalization. I recall hearing a math talk once in which the speaker made a pretty good case that mathematicians who research infinities end up in therapy.
I suspect — <i>suspect</i> — part of your intuition of a problem here is that you're asking, what if we consider multiple encodings, so that what is on the diagonal for the permutation in one encoding is not on the diagonal for another encoding? But the diagonal is actually defined by its hardcoding into the algorithm of A — even more specifically, it's defined by its hardcoding into the algorithm of A<sup>i</sup>. So each A<sup>i</sup> has its own diagonal that it implements.
<i>[edit: tried to straighten out somewhat muddled phrasing re 'what is on the diagonal' for one encoding versus another]</i>Mon, 24 Apr 2017 16:20:30 +0000John ShuttA refutation of Gödel's first incompleteness theoremThe abstraction is normally
http://lambda-the-ultimate.org/node/5425#comment-94188
The abstraction is normally designed so that the abstract machine will terminate (with a loss of precision in the output being calculated). So it is a form of simulation, but of a less powerful class of machine. It would not execute the simulation of the more powerful machine.
e.g. \(L^i\) would not execute the TM encoded in language \(i\) - but it would instead abstract it to an encoding on a less powerful machine. So \(L^i\) would not simulate a Turing Machine as such, but rather a less powerful type of machine that approximates the execution of the machine that \(L^i\) should infer something about.Mon, 24 Apr 2017 12:04:53 +0000Andrew MossA refutation of Gödel's first incompleteness theoremOf course you are right
http://lambda-the-ultimate.org/node/5425#comment-94187
<p>Of course you are right. And in my "detail" comment there was something missing: L machines don't build tables, some other builder agent does, using L machines.
<p>I was trying to focus in the difference between the ( C<sup>i</sup>(A<sup>k</sup>), z ) cell in the T<sup>i</sup> table (not a diagonal cell) and the ( C<sup>k</sup>(A<sup>k</sup>), z ) cell in the T<sup>k</sup> table (a diagonal cell). Of course the content should be the same, as you have clearly shown.
<p>When you focus on the n,n cell in your post, that corresponds to (
C<sup>k</sup>(A<sup>k</sup>), z ) here, and you find undecidability, it is the
builder agent for the table, using L<sup>k</sup>, C<sup>k</sup>(A<sup>k</sup>),
and z, that finds it, right? Of course, if the table is in the head of the
meta-mathematician, the builder agent will be the actual A machine; if the
table can be in an oracle, the agent would be something else.
<p>But in the non-diagonal case, the builder agent (supposing some arbitrary
machine that needs to access that cell - not an A machine obviously), with access to an oracle, might take a shortcut and not work out the output of A<sup>k</sup>(z), and be decidable. Simply follow the steps you prescribe in the rest of the paragraph after focusing in the n,n cell, with a non diagonal ( C<sup>i</sup>(A<sup>k</sup>), z ), and it doesn't work: Just ask the oracle for the diagonal z cell, without bothering with the corresponding machine, and do what A has to do with it. We are filling a totally different cell in a different table, so no problem.
<p>In the diagonal case, the builder agent (a Turing machine?) would be unable to
avoid undecidability. Is this significant? If correct, does this make the
tables (and so the A machines) dependent on the encoding?
Mon, 24 Apr 2017 06:43:22 +0000Enrique Perez ArnaudA refutation of Gödel's first incompleteness theoremIt seems clear to me that
http://lambda-the-ultimate.org/node/5425#comment-94186
<blockquote>
It seems clear to me that undecidability happens in different steps for L<sup>i</sup>( C<sup>i</sup>(A<sup>i</sup>), x ) than for L<sup>k</sup>( C<sup>k</sup>(A<sup>i</sup>), x). In the first case, undecidability is immediate; in the second case, undecidability comes from the need to compute L<sup>i</sup>( C<sup>i</sup>(A<sup>i</sup>), x).
</blockquote>
No. The choice of encoding k has no effect on the behavior of the encoded machine; it doesn't matter that, in this particular case, the encoded machine happens to be one that, <i>internally</i>, uses encoding i.
L<sup>j</sup>(C<sup>j</sup>(f),x)) uses a certain logic, L, to deduce the behavior of a machine f on an input x. The deduction depends on three things: the algorithm of L, the algorithm of f, and the input string x. It does not depend on the choice of encoding, j. In the particular case you've been looking at, f=A<sup>i</sup>, the superscript i denotes what encoding this A uses internally for its computation. That is, A<sup>i</sup> and A<sup>j</sup> are algorithmically different. But C<sup>i</sup>(A<sup>i</sup>) and C<sup>k</sup>(A<sup>i</sup>) are just two different encodings of the <i>same</i> machine, which happens to be A<sup>i</sup>. The k-encoding of A<sup>i</sup> is an encoding of a machine that internally uses encoding i. And as long as logic engine L<sup>k</sup> is given an encoding of A<sup>i</sup> in the encoding it knows how to read, k, it uses the rules of L to make deductions about the behavior of the encoded machine, A<sup>i</sup>.
There is no leakage of the encoding choice j into the behavior of the encoded machine A<sup>i</sup>.Sun, 23 Apr 2017 20:38:07 +0000John ShuttA refutation of Gödel's first incompleteness theoremOkay
http://lambda-the-ultimate.org/node/5425#comment-94185
<p>I can concede that it is not <strong>needed</strong> that the table is an
oracle. The looping argumant is invalid.
<p>However, it is also not needed that it isn't. We can assume it is an oracle,
even though we don't need to assume that. But doing it helps isolate the
problem I am trying to pinpoint.
<p>It seems clear to me that undecidability happens in different steps for
L<sup>i</sup>( C<sup>i</sup>(A<sup>i</sup>), x ) than for L<sup>k</sup>( C<sup>k</sup>(A<sup>i</sup>), x). In the first case, undecidability is
immediate; in the second case, undecidability comes from the need to compute
L<sup>i</sup>( C<sup>i</sup>(A<sup>i</sup>), x).
<p>Confining the table to an oracle helps to isolate the different steps at which
undecidability happens. It surfaces the difference between L<sup>i</sup>( C<sup>i</sup>(A<sup>i</sup>), x ) and L<sup>k</sup>( C<sup>k</sup>(A<sup>i</sup>), x).
<p>So, is there any reason the table cannot be in an oracle? In your post, you
say: "...and we've conspicuously placed no constraints at all on O, not even
computability".
Sun, 23 Apr 2017 14:50:04 +0000Enrique Perez ArnaudA refutation of Gödel's first incompleteness theoremNevertheless, you can't make
http://lambda-the-ultimate.org/node/5425#comment-94184
<blockquote>Nevertheless, you can't make deductions about non-halting that way, so it makes sense that L probably wouldn't be limited to only things that can be deduced by simulation.</blockquote>
Haven't been following too closely, but would abstract interpretation be considered simulation? Because you can infer termination properties using AI.Sun, 23 Apr 2017 13:09:19 +0000naaskingA refutation of Gödel's first incompleteness theoremlooking this over
http://lambda-the-ultimate.org/node/5404#comment-94183
That "LEARNED" idea is just one more thing you have to explain to the user.
Maybe I'll get rid of it. The fewer ideas I have to explain to the user the better.
Sun, 23 Apr 2017 03:25:29 +0000Josh ScholarDomain specific language for playing gamesLanguage for beginners
http://lambda-the-ultimate.org/node/5404#comment-94182
Edit: How do I get this to preserve tabs in code blocks?
This is a language for beginners.
It's a simple statically typed language.
Types are:
integers
real numbers
strings (which are really implemented as interned strings or atoms, because that was convenient for me)
position
direction
enumerated types, including some predefined ones like "player" and "piece_name" also piece(ie slot on the board holding a piece and a player) will be treated like an enumerated type even if the number of slots is variable. Also there are types like enumerated types that are not "enumerated" instead they're the names are learned from context.
sets
maps (something like an array but mapping from a finite type to any value)
arrays
record types - only used to initialize properties that the engine needs.
You can do arithmetic on some non-number types. A direction can be added or subtracted from a position to make a new position. A direction can be added or subtracted from a direction to make a new direction.
an enumerated type definition looks like
<code>player IS { white, black }</code>
a learned enumerator looks like:
<code>zone IS LEARNED</code>
A use of some of these types could be regions on the board where pawn promote and of the region where pawns can make an extra move.
Because those regions are different depending on the player that would be map from player to a list of sets of positions.
In a header of types the engine needs that's written as:
<code>zone IS LEARNED
ENGINE CONSTANT region OF MAP player => MAP zone => SET OF position</code>
Note that case is not significant for keywords. I make them upper case in these examples to set them apart.
A definition of region could look like:
<code>
region = {
white = {
promotion_zone=
{
a8, b8, c8, d8, e8, f8, g8, h8,
},
third_rank=
{
a3, b3, c3, d3, e3, f3, g3, h3,
},
},
black = {
promotion_zone=
{
a1, b1, c1, d1, e1, f1, g1, h1,
},
third_rank=
{
a6, b6, c6, d6, e6, f6, g6, h6,
},
},
}
</code>
Here <code>promotion_zone</code> and <code>third_rank</code> are the enumerated values that <code>zone</code> takes, and it's learned from use in context instead of being explicitly set out before hand.
A few slightly unusual innovations:
The boolean type is called <code>"WHETHER x."</code> and where "x" is a comment and the values are <code>"YES"</code> and <code>"NO"</code> not "true" and "false".
So a routine tests whether a piece if threatened might look like this:
<code>FUNCTION slide_threaten(dir OF direction) RETURNING whether threatened.
shift(dir)
IF is_target() THEN RETURN YES ENDIF
WHILE empty() DO
shift(dir)
IF is_target() THEN RETURN YES ENDIF
ENDWHILE
RETURN NO
ENDFUNCTION</code> Sun, 23 Apr 2017 03:12:14 +0000Josh ScholarDomain specific language for playing games