[Haskell-cafe] Slightly off-topic: Lambda calculus
OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
forgot to cc the cafe :-) On Sun, Jun 21, 2009 at 1:08 PM, Keith Sheppardkeiths...@gmail.com wrote: hmm, it's been a while but... i think this infinite loop with a free variable would cause collision (\a . a a) (\b . b b d) On Sun, Jun 21, 2009 at 12:53 PM, Andrew Coppinandrewcop...@btinternet.com wrote: OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- keithsheppard.name -- keithsheppard.name ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
An answer would probably depend on the reductions order you've chosen. Would that do? (\e - e (\u - e (\v - u))) (\f - \x - f x) -- all variables have different names, see? = (\f - \x - f x) (\u - (\f - \x - f x) (\v - u)) = \x - (\u - (\f - \x - f x) (\v - u)) x = \x - (\f - \x - f x) (\v - x) = \x - \x - (\v - x) x -- Ouch! = \x - \x - x = \x - id where the real answer is \x - (\f - \x - f x) (\v - x) = \x - (\f - \y - f y) (\v - x) = \x - \y - (\v - x) y = \x - \y - x = \x - const x On 21 Jun 2009, at 20:53, Andrew Coppin wrote: OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
On Sun, Jun 21, 2009 at 8:53 PM, Andrew Coppinandrewcop...@btinternet.com wrote: OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. It seems obvious scince beta reduction never introduces new variales... -- Victor Nazarov ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
2009/6/21 Andrew Coppin andrewcop...@btinternet.com: OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. I'm no expert, but it sounds to me like you're doing the equivalent of de Bruijn indexing, which is a method to avoid alpha conversion, which is basically what you're worried about. Therefore, I'm guessing that there will be no name collisions. -- Deniz Dogan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
Correction: I think that one can find an expression that causes name clashes anyway, I'm just not certain that there is one that would clash independent of whichever order you choose. On 21 Jun 2009, at 21:12, Miguel Mitrofanov wrote: An answer would probably depend on the reductions order you've chosen. Would that do? (\e - e (\u - e (\v - u))) (\f - \x - f x) -- all variables have different names, see? = (\f - \x - f x) (\u - (\f - \x - f x) (\v - u)) = \x - (\u - (\f - \x - f x) (\v - u)) x = \x - (\f - \x - f x) (\v - x) = \x - \x - (\v - x) x -- Ouch! = \x - \x - x = \x - id where the real answer is \x - (\f - \x - f x) (\v - x) = \x - (\f - \y - f y) (\v - x) = \x - \y - (\v - x) y = \x - \y - x = \x - const x On 21 Jun 2009, at 20:53, Andrew Coppin wrote: OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
scratch that... it's completely wrong On Sun, Jun 21, 2009 at 1:09 PM, Keith Sheppardkeiths...@gmail.com wrote: forgot to cc the cafe :-) On Sun, Jun 21, 2009 at 1:08 PM, Keith Sheppardkeiths...@gmail.com wrote: hmm, it's been a while but... i think this infinite loop with a free variable would cause collision (\a . a a) (\b . b b d) On Sun, Jun 21, 2009 at 12:53 PM, Andrew Coppinandrewcop...@btinternet.com wrote: OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- keithsheppard.name -- keithsheppard.name -- keithsheppard.name ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
On Sun, Jun 21, 2009 at 05:53:04PM +0100, Andrew Coppin wrote: I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? With name collisions I'm assuming you mean inadvertent variable capture. The answer depends on your evaluation strategy. If you never reduce inside a lambda (e.g. call-by-name or call-by-value), then you will always be substituting a closed term in place of a variable, and nothing in a closed term can get captured. However, if by as many reductions as possible you mean to normal form, then you also need to reduce inside lambdas. Then the story is different. Consider the following sequence of beta reductions: (\x. x x) (\y. \z. y z) - (\y. \z. y z) (\y. \z. y z) - \z. (\y. \z. y z) z - \z. \z'. z z' Notice that in the original form, all variable names were unique, but then the variable z got duplicated, and the last reduction happened _inside_ the \z. expression, which required renaming of the inner z in order to avoid variable capture and the erroneous result of \z. \z. z z. Hope this helps. Lauri ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
On Sun, Jun 21, 2009 at 05:53:04PM +0100, Andrew Coppin wrote: OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. Lambda calculus is one of those things that seems simple in theory (because it IS simple in theory) but can be tricky to implement correctly. I recommend reading the first few chapters of Benjamin Pierce's Types and Programming Languages for a good discussion of the issues involved (including explanations and implementations of both a named style, and a de Bruijn index style), and then also I am not a number, I am a free variable by McBride and McKinna, which explains a locally nameless style which mixes the best of both worlds. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
Miguel Mitrofanov wrote: Correction: I think that one can find an expression that causes name clashes anyway, I'm just not certain that there is one that would clash independent of whichever order you choose. Yes there is. Consider (\f g - f (f (f (f (f (f g)) (\l a b - l (b a)) (\x - x) which has 6 variables in total. This reduces to the normal form \a b c d e f g - g (f (e (d (c (b a) which requires 7 variables. So without alpha-conversion at least one of the original 6 variables will clash with itself. Bertram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
Lauri Alanko wrote: With name collisions I'm assuming you mean inadvertent variable capture. The answer depends on your evaluation strategy. If you never reduce inside a lambda (e.g. call-by-name or call-by-value), then you will always be substituting a closed term in place of a variable, and nothing in a closed term can get captured. However, if by as many reductions as possible you mean to normal form, then you also need to reduce inside lambdas. Then the story is different. Consider the following sequence of beta reductions: (\x. x x) (\y. \z. y z) - (\y. \z. y z) (\y. \z. y z) - \z. (\y. \z. y z) z - \z. \z'. z z' Notice that in the original form, all variable names were unique, but then the variable z got duplicated, and the last reduction happened _inside_ the \z. expression, which required renaming of the inner z in order to avoid variable capture and the erroneous result of \z. \z. z z. Hope this helps. Ladies and gentlemen, we have a counter-example! (\x1 - x1 x1) (\y2 - \z3 - y2 z3) (\y2 - \z3 - y2 z3) (\y2 - \z3 - y2 z3) \z3 - (\y2 - \z3 - y2 z3) z3 \z3 - \z3 - z3 z3 This *should* of course be \z3 - \z4 - z3 z4 which is a different function. Now the operative question becomes... how in the name of God to I fix this? (The obvious approach would be to rerun the renamer; but would discarding the variable indicies introduce even more ambiguity? Hmm...) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
Wow. Now you've showed it to me, it seems pretty obvious. That's what I like about math. On 21 Jun 2009, at 21:56, Bertram Felgenhauer wrote: Miguel Mitrofanov wrote: Correction: I think that one can find an expression that causes name clashes anyway, I'm just not certain that there is one that would clash independent of whichever order you choose. Yes there is. Consider (\f g - f (f (f (f (f (f g)) (\l a b - l (b a)) (\x - x) which has 6 variables in total. This reduces to the normal form \a b c d e f g - g (f (e (d (c (b a) which requires 7 variables. So without alpha-conversion at least one of the original 6 variables will clash with itself. Bertram ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
Probably the easiest way to fix this was already proposed by Deniz Dogan: de Bruijn indices. On 21 Jun 2009, at 21:57, Andrew Coppin wrote: Lauri Alanko wrote: With name collisions I'm assuming you mean inadvertent variable capture. The answer depends on your evaluation strategy. If you never reduce inside a lambda (e.g. call-by-name or call-by-value), then you will always be substituting a closed term in place of a variable, and nothing in a closed term can get captured. However, if by as many reductions as possible you mean to normal form, then you also need to reduce inside lambdas. Then the story is different. Consider the following sequence of beta reductions: (\x. x x) (\y. \z. y z) - (\y. \z. y z) (\y. \z. y z) - \z. (\y. \z. y z) z - \z. \z'. z z' Notice that in the original form, all variable names were unique, but then the variable z got duplicated, and the last reduction happened _inside_ the \z. expression, which required renaming of the inner z in order to avoid variable capture and the erroneous result of \z. \z. z z. Hope this helps. Ladies and gentlemen, we have a counter-example! (\x1 - x1 x1) (\y2 - \z3 - y2 z3) (\y2 - \z3 - y2 z3) (\y2 - \z3 - y2 z3) \z3 - (\y2 - \z3 - y2 z3) z3 \z3 - \z3 - z3 z3 This *should* of course be \z3 - \z4 - z3 z4 which is a different function. Now the operative question becomes... how in the name of God to I fix this? (The obvious approach would be to rerun the renamer; but would discarding the variable indicies introduce even more ambiguity? Hmm...) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
Andrew Coppin wrote: Ladies and gentlemen, we have a counter-example! (\x1 - x1 x1) (\y2 - \z3 - y2 z3) (\y2 - \z3 - y2 z3) (\y2 - \z3 - y2 z3) \z3 - (\y2 - \z3 - y2 z3) z3 \z3 - \z3 - z3 z3 Now the operative question becomes... how in the name of God to I fix this? (The obvious approach would be to rerun the renamer; but would discarding the variable indicies introduce even more ambiguity? Hmm...) I knew alpha conversions were trixy little things! ;-) Well anyway, the obvious thing to do is after each reduction, strip off all the variable indicies and rerun the labeller to assign new indicies. But does this solution work properly in general? The labeller is carefully crafted to respect scoping, so that for example \x - x (\x - x) x becomes \x1 - x1 (\x2 - x2) x1. But still, the final expression above is nicely labelled, yet wrong. How does this happen? Well, variable indicies are supposed to be unique. But in line 2 we see a bunch of them get duplicated. At this point, if you strip all the indicies and recompute them, you get (\y1 - \z2 - y1 z2) (\y3 - \z4 - y3 z4) There are now no spurious duplicates, and the reduction should proceed through the remaining steps without incident. So rerunning the labeller works *for this example*. But does it work in general? As an alternative, I could completely reprogram my entire application to use de Bruijn indices. Hmm... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
Andrew Coppin wrote: Well anyway, the obvious thing to do is after each reduction, strip off all the variable indicies and rerun the labeller to assign new indicies. But does this solution work properly in general? No. Supposing some Lambda expression eventually reduces to, say, \x1 - \x2 - x1 x2 Now strip off all the indicies: \x - \x - x x ...and recompute them... \x1 - \x2 - x2 x2 FAIL. To make it worth properly, I would have to (at least) make the renamer respect any indicies which are already present. It's nontrivial, but doable. Of course, the £1,643,264 question is... would it work even then? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
Hello, Have you read the lambda calculus chapter in: The Implementation of Functional Programming Languages by Simon Peyton Jones, published by Prentice Hall, 1987: http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/ - jeremy ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
As others have pointed out, it is not enough to rename before reduction. It should be pretty obvious since when you do substitution and copy a lambda expression into more than once place you will introduce variables with the same name. You can keep unique variables by cloning during substitution, i.e., renaming the bound variables. -- Lennart On Sun, Jun 21, 2009 at 6:53 PM, Andrew Coppinandrewcop...@btinternet.com wrote: OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
Actually, keeping all names distinct is not de Bruijn numbering, it's called the Barendregt convention. On Sun, Jun 21, 2009 at 7:05 PM, Deniz Dogandeniz.a.m.do...@gmail.com wrote: 2009/6/21 Andrew Coppin andrewcop...@btinternet.com: OK, so I'm guessing there might be one or two (!) people around here who know something about the Lambda calculus. I've written a simple interpretter that takes any valid Lambda expression and performs as many beta reductions as possible. When the input is first received, all the variables are renamed to be unique. Question: Does this guarantee that the reduction sequence will never contain name collisions? I have a sinking feeling that it does not. However, I can find no counter-example as yet. If somebody here can provide either a proof or a counter-example, that would be helpful. I'm no expert, but it sounds to me like you're doing the equivalent of de Bruijn indexing, which is a method to avoid alpha conversion, which is basically what you're worried about. Therefore, I'm guessing that there will be no name collisions. -- Deniz Dogan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
On Sun, Jun 21, 2009 at 07:48:30PM +0100, Andrew Coppin wrote: Andrew Coppin wrote: Well anyway, the obvious thing to do is after each reduction, strip off all the variable indicies and rerun the labeller to assign new indicies. But does this solution work properly in general? No. Supposing some Lambda expression eventually reduces to, say, \x1 - \x2 - x1 x2 Now strip off all the indicies: \x - \x - x x ...and recompute them... \x1 - \x2 - x2 x2 FAIL. To make it worth properly, I would have to (at least) make the renamer respect any indicies which are already present. It's nontrivial, but doable. Of course, the £1,643,264 question is... would it work even then? I reiterate the pointers to reading material that I gave earlier. A lot of really smart people have spent a lot of time thinking about this already; it's likely not worth any more of your time to try figuring it out yourself. (It's definitely worth some initial time struggling with it, so that you can properly appreciate the solutions---but it sounds like you've already done that!) Briefly, the key operation is substitution---*while* doing a substitution you have to somehow check that names aren't clashing, and possibly rename some things if necessary (or if using de Bruijn indices, you may need to shift some indices around while doing substitution). If you wait until *after* doing a substitution to fix up the names, it's too late. But don't take my word for it, go read about it somewhere. =) -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic: Lambda calculus
All, Just as ancillary information: ∃ a calculator on Hackage called LambdaCalculator. Its rather short (loc wise) and fun to play with. Thomas On Sun, Jun 21, 2009 at 10:57 AM, Andrew Coppinandrewcop...@btinternet.com wrote: Lauri Alanko wrote: With name collisions I'm assuming you mean inadvertent variable capture. The answer depends on your evaluation strategy. If you never reduce inside a lambda (e.g. call-by-name or call-by-value), then you will always be substituting a closed term in place of a variable, and nothing in a closed term can get captured. However, if by as many reductions as possible you mean to normal form, then you also need to reduce inside lambdas. Then the story is different. Consider the following sequence of beta reductions: (\x. x x) (\y. \z. y z) - (\y. \z. y z) (\y. \z. y z) - \z. (\y. \z. y z) z - \z. \z'. z z' Notice that in the original form, all variable names were unique, but then the variable z got duplicated, and the last reduction happened _inside_ the \z. expression, which required renaming of the inner z in order to avoid variable capture and the erroneous result of \z. \z. z z. Hope this helps. Ladies and gentlemen, we have a counter-example! (\x1 - x1 x1) (\y2 - \z3 - y2 z3) (\y2 - \z3 - y2 z3) (\y2 - \z3 - y2 z3) \z3 - (\y2 - \z3 - y2 z3) z3 \z3 - \z3 - z3 z3 This *should* of course be \z3 - \z4 - z3 z4 which is a different function. Now the operative question becomes... how in the name of God to I fix this? (The obvious approach would be to rerun the renamer; but would discarding the variable indicies introduce even more ambiguity? Hmm...) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic
On 11/1/07, PR Stanley [EMAIL PROTECTED] wrote: If anyone knows anything about the rules of proof by deduction and quantifiers I'd be grateful for some assistance. I'm currently doing a course on Type Theory which includes proving by natural deduction. See, among other things, the course notes on: http://www.cs.ru.nl/~freek/courses/tt-2007 regards, Bas van Dijk ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Slightly off-topic
Hi folks Apologies for the off-topic post. If anyone knows anything about the rules of proof by deduction and quantifiers I'd be grateful for some assistance. Much obliged, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Slightly off-topic
prstanley: Hi folks Apologies for the off-topic post. If anyone knows anything about the rules of proof by deduction and quantifiers I'd be grateful for some assistance. Much obliged, http://www.cs.cmu.edu/~rwh/plbook/ Is an excellent introduction to reasoning about programming languages. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Slightly Off-topic
Hi Does anyone know of a good active list for students and experts in discrete mathematics, in particular, logic? Thanks, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
