So it sounds like #[...] is the inverse operation of &..., but can only be used within quotes.
No, that doesn’t make sense to me. The inverse of & would be a computable function that takes the Gödel number of a unary numeral and returns the number represented by that numeral. #[...] is syntactic sugar somewhat similar to the $NAME in e.g. Perl’s “Hello, $NAME!”. But--
So in “#[&n] >= 7” = ge(&n, &7), why do you have “#[&n]” instead of just “n”? Is that to make it clear that you’re using the numeric value of n rather than the variable n?
Well, it’s because “n >= 7” would mean an expression that contains the variable n, rather than an expression containing the unary numeral representing the numeric value of n. (“n >= 7″ = ge(‘n’, &7) is a different Gödel number than “#[&n] >= 7” = ge(&n, &7).) Being able to distinguish between such meanings was the point of introducing the explicit notation, because in my original post it was unclear what I meant and I confused myself enough that I ended up with a buggy proof. Possibly we’re at least part-way there to understanding each other, but you’re conceptualizing things differently?
Also, what does ”… #&F …” mean? From my understanding, that would get unpacked as subst(repr(F), repr(#[repr(m)])), but that is a syntax error.
No, wait, that’s completely wrong. We need to distinguish between applying repr(.) to an argument and constructing the Gödel number of an expression in which repr(.) is applied to an argument. For example, in my earlier comment, plus(x,y) was not equal to (x+y): if x and y are the Gödel numbers of two expressions, then (x+y) would simply add those Gödel numbers (which isn’t useful), whereas plus(x,y) returns the Gödel number of an expression (namely the expression adding the expressions denoted by the Gödel numbers x and y). Do you see what I mean?
Perhaps it would be good to have a common prefix for functions that construct the Gödel numbers of expressions: replace plus(.,.) and ge(.,.) from the previous post by mkPlus(.,.) and mkGe(.,.), and add the function mkRepr(e), which constructs the expression that applies repr to the expression denoted by e, and mkSubst(e1,e2), which constructs the expression that applies subst to the expressions denoted by e1 and e2. Let’s also have mkEq(.) for equality. Then, we have
(I’ll continue to write the Gödel number of a variable by putting the variable in quotes, because it doesn’t seem helpful to introduce another notation for that.) As another example, we have
So the middle “&” gets translated to mkRepr, because it is inside the quotes; but the other two &’s are just repr(.), because they are inside the splice, which means that they are not quoted.
No, that doesn’t make sense to me. The inverse of & would be a computable function that takes the Gödel number of a unary numeral and returns the number represented by that numeral. #[...] is syntactic sugar somewhat similar to the $NAME in e.g. Perl’s “Hello, $NAME!”.
But “#[&7]” = “7″, and if you replace the 7s with some other number, it’s still true, right?
“n >= 7” would mean an expression that contains the variable n, rather than an expression containing the unary numeral representing the numeric value of n.
Got it.
No, wait, that’s completely wrong. We need to distinguish between applying repr(.) to an argument and constructing the Gödel number of an expression in which repr(.) is applied to an argument. For example, in my earlier comment, plus(x,y) was not equal to (x+y): if x and y are the Gödel numbers of two expressions, then (x+y) would simply add those Gödel numbers (which isn’t useful), whereas plus(x,y) returns the Gödel number of an expression (namely the expression adding the expressions denoted by the Gödel numbers x and y). Do you see what I mean?
Oh, I see. Everything after that paragraph, I’m going to have to think about for a while. Edit: got it (I think).
But “#[&7]” = “7″, and if you replace the 7s with some other number, it’s still true, right?
Ah! This is correct, but I would conceptualize it differently, as the combination of two distinct phenomena. First, #[...] is sort of the inverse of ”...”, which makes more sense to me because both of these are kinds of syntactic sugar—we have both “#[e]” = e and “x + #[‘y’]” = “x + y”.
Second, “7” is the Gödel number of the unary numeral 7, and repr(7) also returns this Gödel number. In other words, “7“ = &7. Putting the two together: “#[&7]” = &7 = “7”.
...although the mkStuff way of writing things is ugly in one way: it means that if you want to desugar quotes inside quotes, you may need to introduce mkMkStuff functions, as in,
(Recall that ‘a’ denotes the Gödel number of the variable a; repr(‘a’) is the Gödel number of an expression that evaluates to the Gödel number of a, which is what we need in that place.)
It would be better to introduce functions call(name,arg) and pair(x,y) such that
No, that doesn’t make sense to me. The inverse of & would be a computable function that takes the Gödel number of a unary numeral and returns the number represented by that numeral. #[...] is syntactic sugar somewhat similar to the $NAME in e.g. Perl’s “Hello, $NAME!”. But--
Well, it’s because “n >= 7” would mean an expression that contains the variable n, rather than an expression containing the unary numeral representing the numeric value of n. (“n >= 7″ = ge(‘n’, &7) is a different Gödel number than “#[&n] >= 7” = ge(&n, &7).) Being able to distinguish between such meanings was the point of introducing the explicit notation, because in my original post it was unclear what I meant and I confused myself enough that I ended up with a buggy proof. Possibly we’re at least part-way there to understanding each other, but you’re conceptualizing things differently?
No, wait, that’s completely wrong. We need to distinguish between applying repr(.) to an argument and constructing the Gödel number of an expression in which repr(.) is applied to an argument. For example, in my earlier comment, plus(x,y) was not equal to (x+y): if x and y are the Gödel numbers of two expressions, then (x+y) would simply add those Gödel numbers (which isn’t useful), whereas plus(x,y) returns the Gödel number of an expression (namely the expression adding the expressions denoted by the Gödel numbers x and y). Do you see what I mean?
Perhaps it would be good to have a common prefix for functions that construct the Gödel numbers of expressions: replace plus(.,.) and ge(.,.) from the previous post by mkPlus(.,.) and mkGe(.,.), and add the function mkRepr(e), which constructs the expression that applies repr to the expression denoted by e, and mkSubst(e1,e2), which constructs the expression that applies subst to the expressions denoted by e1 and e2. Let’s also have mkEq(.) for equality. Then, we have
(I’ll continue to write the Gödel number of a variable by putting the variable in quotes, because it doesn’t seem helpful to introduce another notation for that.) As another example, we have
Now, the example you quote:
So the middle “&” gets translated to mkRepr, because it is inside the quotes; but the other two &’s are just repr(.), because they are inside the splice, which means that they are not quoted.
But “#[&7]” = “7″, and if you replace the 7s with some other number, it’s still true, right?
Got it.
Oh, I see. Everything after that paragraph, I’m going to have to think about for a while. Edit: got it (I think).
Ah! This is correct, but I would conceptualize it differently, as the combination of two distinct phenomena. First, #[...] is sort of the inverse of ”...”, which makes more sense to me because both of these are kinds of syntactic sugar—we have both “#[e]” = e and “x + #[‘y’]” = “x + y”.
Second, “7” is the Gödel number of the unary numeral 7, and repr(7) also returns this Gödel number. In other words, “7“ = &7. Putting the two together: “#[&7]” = &7 = “7”.
:-) Thanks again for sticking with it!
...although the mkStuff way of writing things is ugly in one way: it means that if you want to desugar quotes inside quotes, you may need to introduce mkMkStuff functions, as in,
(Recall that ‘a’ denotes the Gödel number of the variable a; repr(‘a’) is the Gödel number of an expression that evaluates to the Gödel number of a, which is what we need in that place.)
It would be better to introduce functions call(name,arg) and pair(x,y) such that
etc. Then we can apply the desugaring recursively--
HTH more than it confuses :-/