 |
|
|
|
|
|
| |
| |
|
|
|
|
| |
| |
|
|
when I read something like this...
http://www.irregularwebcomic.net/
--
Darren New, San Diego CA, USA (PST)
Insanity is a small city on the western
border of the State of Mind.
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Darren New wrote:
> when I read something like this...
>
> http://www.irregularwebcomic.net/
Why thank you. :-/
In a stunning turn of events, I was just in the middle of having a
conversation about whether assigning unique indicies to every variable
in a Lambda expression enables its reduction sequence to be computed
without name clashes. :-P
--
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
Orchid XP v8 wrote:
> Darren New wrote:
>> when I read something like this...
>>
>> http://www.irregularwebcomic.net/
>
> Why thank you. :-/
That was a complement. :-)
Along the lines of "Gee, I bet Andrew, with some practice, could also turn
out a blog full of interesting discussions of abstruse mathematical proofs
that would garner a world-wide audience, too."
--
Darren New, San Diego CA, USA (PST)
Insanity is a small city on the western
border of the State of Mind.
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
"Darren New" <dne### [at] san rrcom> wrote in message
news:4a3e7769$1@news.povray.org...
> Orchid XP v8 wrote:
> > Darren New wrote:
> >> when I read something like this...
> >> http://www.irregularwebcomic.net/
> > Why thank you. :-/
> That was a complement. :-)
And two's, no less.
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
>> Why thank you. :-/
>
> That was a complement. :-)
>
> Along the lines of "Gee, I bet Andrew, with some practice, could also
> turn out a blog full of interesting discussions of abstruse mathematical
> proofs that would garner a world-wide audience, too."
1. What makes you think anybody reads that blog?
2. Every time I write... well, virtually anything, actually... almost
nobody reads it. Which is mainly why I seldom write anything.
--
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
On 21-6-2009 20:00, Orchid XP v8 wrote:
> Darren New wrote:
>> when I read something like this...
>>
>> http://www.irregularwebcomic.net/
>
> Why thank you. :-/
>
> In a stunning turn of events, I was just in the middle of having a
> conversation about whether assigning unique indicies to every variable
> in a Lambda expression enables its reduction sequence to be computed
> without name clashes. :-P
>
There is alpha conversion to prevent that, but I guess you are talking
about an implementation not the theory. ;)
I seem to remember that labelling just with the level of the nesting is
enough. If you have unique identifiers throughout your program, that
certainly works.
On a similar note, assigning unique indices to the lambdas gives an
almost trivial way to prove that lambda calculus is Church-Rosser. At
least I think so, I have never seen that in a paper, so there might be a
complication that I missed.
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
>> In a stunning turn of events, I was just in the middle of having a
>> conversation about whether assigning unique indicies to every variable
>> in a Lambda expression enables its reduction sequence to be computed
>> without name clashes. :-P
>
> There is alpha conversion to prevent that, but I guess you are talking
> about an implementation not the theory. ;)
Indeed. It's significantly less trivial than you'd imagine... o_O
> I seem to remember that labelling just with the level of the nesting is
> enough.
That would be de Bruijn indices. And I'm hoping to avoid needing to go
that far... (But we'll see!)
> If you have unique identifiers throughout your program, that
> certainly works.
Ah, but wait. Simply renaming all the variables before you start is
insufficient. Unfortunately.
(\x -> x x) (\y -> y)
Make 'em all unique:
(\x1 -> x1 x1) (\y2 -> y2)
Now beta-reduce:
(\y2 -> y2) (\y2 -> y2)
Oh noes! No longer unique...
(In this instance it doesn't matter, but somebody showed me a slightly
more complicated example where it actually goes wrong.)
--
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
On 21-6-2009 21:40, Orchid XP v8 wrote:
>>> In a stunning turn of events, I was just in the middle of having a
>>> conversation about whether assigning unique indicies to every
>>> variable in a Lambda expression enables its reduction sequence to be
>>> computed without name clashes. :-P
>>
>> There is alpha conversion to prevent that, but I guess you are talking
>> about an implementation not the theory. ;)
>
> Indeed. It's significantly less trivial than you'd imagine... o_O
>
>> I seem to remember that labelling just with the level of the nesting
>> is enough.
>
> That would be de Bruijn indices. And I'm hoping to avoid needing to go
> that far... (But we'll see!)
It requires a different implementation and different data structures,
but as you already have proven that the other path is infeasible...
Having named bound variables is very natural if you were brought up in
imperative languages, but I don't see the point in functional languages,
other than in the human interface.
>
>> If you have unique identifiers throughout your program, that certainly
>> works.
>
> Ah, but wait. Simply renaming all the variables before you start is
> insufficient. Unfortunately.
>
> (\x -> x x) (\y -> y)
>
> Make 'em all unique:
>
> (\x1 -> x1 x1) (\y2 -> y2)
>
> Now beta-reduce:
>
> (\y2 -> y2) (\y2 -> y2)
>
> Oh noes! No longer unique...
>
> (In this instance it doesn't matter, but somebody showed me a slightly
> more complicated example where it actually goes wrong.)
>
I didn't realize you would want to use them at run-time (bad idea IMHO,
see above). Not your fault, I just did not read carefully.
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
>>> I seem to remember that labelling just with the level of the nesting
>>> is enough.
>>
>> That would be de Bruijn indices. And I'm hoping to avoid needing to go
>> that far... (But we'll see!)
>
> It requires a different implementation and different data structures,
> but as you already have proven that the other path is infeasible...
> Having named bound variables is very natural if you were brought up in
> imperative languages, but I don't see the point in functional languages,
> other than in the human interface.
My whole program is "human interface". It doesn't do anything "useful",
it's just to allow a human being to easily observe the reduction
sequence. To that end, I'd like the program to avoid screwing around
with the human-provided variables names as much as is feasible. OTOH,
I'd also like the thing to *work*... ;-)
> I didn't realize you would want to use them at run-time (bad idea IMHO,
> see above). Not your fault, I just did not read carefully.
Well, I think if I can relabel the variables after each expression
transformation to recover uniqueness, it should work.
(Unfortunately the labeller currently looks only at the variable *names*
and ignores the index values. That means that expressions which already
have indicies can get renamed incorrectly.)
--
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
| |
|
|
On Sun, 21 Jun 2009 19:25:52 +0100, Orchid XP v8 <voi### [at] devnull> wrote:
>2. Every time I write... well, virtually anything, actually... almost
>nobody reads it. Which is mainly why I seldom write anything.
I read your blog a million times more than I read anyone elses.
--
Regards
Stephen
Post a reply to this message
|
|
| |
| |
|
|
|
|
| |
