2

I got quite confused about what is and is not a redex in Haskell, so I spent some time on it, but I would like feedback whether I got it right.

I found this definition of a redex, and it is circular; Etymology : From "reducible expression" Definition: Redex (plural redexes): (mathematics) Something to be reduced according to the rules of a formal system. http://en.wiktionary.org/wiki/redex

The above definition presumes one knows how to reduce. So to me this is like saying "Bluish is the quality of looking blue", which is also circular.

Then I found a blog post that defines redex as follows; Any subgraph that matches a rule is called a reducible expression, or redex for short. https://hackhands.com/lazy-evaluation-works-haskell/

That's much better but, taken literally it means that it is implementation specific, which seems odd. In other words, if I can define myfunc in two different ways with different evaluation trees, the definition of what is a redex would differ. I don't think that is true.

It seems that the important thing is the evaluation parse tree and, in turn, the definition of what is a primitive. I could not find a definition of Haskell primitives, but I found a possibly incomplete list: "Important Haskell primitive functions" http://www.cs.sjsu.edu/faculty/smithj/oldclass/152f11/haskell-primitives.html

Is there a real definition of Haskell primitives that I have missed?

Moving on, the list helps identify some examples of primitives and non-primitives. -- Primitive: *, / , div -- Not-Primitive (not on the list): mul

Putting this all together, it says that a primitive function evaluation is reducible, being a leaf node on the evaluation tree. The reduction reduces from a function call to a data point.

Thus, how is this definition ? Redex: In Haskell, evaluation proceeds with the base case that any primitive function application constitutes a leaf node of the evaluation tree. Such leaves are reducible from function applications into pure data elements. Thus we define all leaf nodes as reducible expressions, or "redexs" for short.

thank you!

Edit; Here are some examples I'm trying to accommodate, that I believe true. The first is from Graham Hutton , Programming in Haskell. -- Consider these cases; -- 1.An expression using a function mult ::(Int, Int)-> Int -- pg.126 mult (x,y) = x*y mult(1+2, 3+4) -- This has 3 redexes, one for each argument and one for the call, per the book

-- 2.Now consider using '*', a primitive, instead of mul, a function, 7 + (6*8) -- This has one redex, only the 6*8, per discussions.

-- 3.Finally, contrast to all primitives without any parentheses to indicate a new evaluation level 1 + 2*3 -- This should have zero redexes, I believe, since they are only primitive expressions which can be evaluated all at once.

AnneTheAgile
  • 9,932
  • 6
  • 52
  • 48
  • 1
    Reason for -1 vote? I have found this circular definition also in Graham Hutton's book, so it seems like an important problem. – AnneTheAgile Dec 21 '14 at 20:56
  • 1
    You can think about what is reducible in terms of the primitives that are internal to an implementation, but you can also think about what is reducible in terms of the language independently of the implementation. For Haskell one version of the latter is "the application of a lambda is reducible. The application of a constructor to a reducible expression is reducible. A lambda is irreducible. The application of a constructor to irreducible expressions is irreducible." – Cirdec Dec 21 '14 at 21:21
  • @Cirdec, hmm, I'm sorry, are you giving me feedback on my proposed definition? If so I'm sorry but I don't understand what parts of my statement you think are true/false? I think I have a smaller crow than most Haskellizers so I apologize for that :). – AnneTheAgile Dec 21 '14 at 22:58
  • 1
    I'm not criticizing your statement, I'm suggesting that you can also consider reduction from the point of view of what the expressions mean rather than how the interpreter is implemented. If you do so, you don't need to make any distinction between primitive functions and those defined by lambdas and function declarations. You can instead think that all functions are "constructed" by lambdas. In either case, any function application is reducible. (Also, I don't even have a crow.) – Cirdec Dec 21 '14 at 23:27
  • @Cirdec, I added some examples to my question. Does that help? I am beginning to see what you mean but then I ask what is a function application? I had thought that applying + was a function application. In the book, all over it has "applying +". Yet it is not always a function application? I'm pretty sure you have a large crow! The first hit for crow epistemology finds two of my friends posting ; http://oncodingstyle.blogspot.com/2008/09/crow-epistemology.html – AnneTheAgile Dec 22 '14 at 00:03
  • 1
    Yes you need to know how to reduce. It's in your formal system definition. Read the wikipedia entry on lambda calculus for example, the reductions are listed there explicitly. – n. m. could be an AI Dec 22 '14 at 06:19
  • 1
    Your final example still has one redex, `2 * 3`. Parentheses don't matter. Also, the definition of "redex" from Wikipedia isn't "circular". The definition refers to the rules of the formal system, yes. So you cannot define what a "redex" is unless you know the formal system. But as long as the rules of the formal system aren't based on what a "redex" is in turn, there's no circularity. – kosmikus Dec 23 '14 at 13:44
  • For Haskell in particular, I am not sure where to find the "rules of the formal system"? – AnneTheAgile Dec 23 '14 at 19:55

1 Answers1

1

A redex in a functional language, once you get past the syntax (i.e. translating 1 + 2 from infix into (+) 1 2) is just anything that looks like f x -- i.e. a function and an argument such that the function has not been applied to the argument.

One shouldn't worry about which things are and aren't "primitive" functions

And in fact, contra-Hutton, I'd say that 1+2 has two redexes, since it is actually uncurried, and so the "desugared" form is ((+) 1) 2.

sclv
  • 38,665
  • 7
  • 99
  • 204