[HN Gopher] Primitive Recursive Functions for a Working Programmer
___________________________________________________________________
Primitive Recursive Functions for a Working Programmer
Author : ingve
Score : 103 points
Date : 2024-08-03 12:32 UTC (10 hours ago)
(HTM) web link (matklad.github.io)
(TXT) w3m dump (matklad.github.io)
| fire_lake wrote:
| Just tackling the first part, about restricted languages being
| better for some applications:
|
| Isn't the advantage that an upper bound on the number of steps
| required can be computed statically?
|
| This means we can refuse to compute things that violate some
| limit and give back a meaningful error, for all possible inputs.
|
| Whereas with the _Turing complete plus Runtime Limit_ approach,
| we might pick a limit that is too low for some inputs we care
| about. We won't know until we run the computation and hit the
| limit! We see this sometimes with C++ template recursion.
|
| I might be totally confused here so I hope some more knowledgable
| can weigh in :)
| mrkeen wrote:
| Accurately predicting fuel usage for a blockchain computation?
| It's probably interesting to others but not to me.
|
| I'd be more interested in using it just as another hammer in
| the tool-belt to squash bugs that got past earlier hammers
| (static type-checking, no nulls, no mutations, etc.)
|
| Terminating in finite time can't prove correctness, but if I
| declare that my code will terminate in finite time and my
| compiler disagrees, I'd certainly believe my code is incorrect.
| hinkley wrote:
| I use 10x the reasonable computation amount, ever since a
| coworker used a number closer to 3x and real workloads hit that
| limit a few years later. I figure giving a bad workflow several
| times longer to fail is still measured in milliseconds and
| doesn't hurt that much.
|
| But I usually run into this problem when someone has treated
| the problem domain as a DAG but can't enforce the Acyclic part.
| But modeling your problem as a DAG is reminiscent of Dark
| Galadriel, when she contemplates taking the arming from Frodo -
| All Shall Love Me and Despair. The people who make them are
| always way prouder of themselves than they deserve to be.
|
| Eventually your customers who were attracted by the expensive
| and complex solution to their problems run out of money, and
| their problems seem a lot smaller to them. Then you are left -
| literally - with an app that cannot be made cheap enough per
| operation to keep their business.
| gopher_space wrote:
| > treated the problem domain as a DAG but can't enforce the
| Acyclic part.
|
| Would you mind talking about this for a bit? I'm missing a
| lot of context.
| kccqzy wrote:
| And what if that upper bound is an extremely loose upper bound?
| Say a deterministic quick sort has an upper bound that's
| quadratic in input size even though typically it's
| linearithmic? Do you refuse the computation of quick sort then?
| Or more dramatically consider the Hindley-Milner algorithm
| which has an upper bound of exponential time even though in
| practice it runs in linear time?
| IshKebab wrote:
| I don't know about "computed statically" but yeah I think the
| only advantage to drastically limiting the capabilities of a
| language (as in many new configuration languages, CEL, etc.) is
| that you can have a sort of computation limit that isn't _data
| dependent_.
|
| But I struggle to think of a single situation in which that's a
| real hard requirement. How many systems are there that can't
| give a "query took too long" error?
| ch0ic3 wrote:
| I'm struggling with the mini rant / motivation of the article:
|
| > Typically, not being Turing-complete is extolled as a virtue or
| even a requirement in specific domains. I claim that most such
| discussions are misinformed -- that not being Turing complete
| doesn't actually mean what folks want it to mean
|
| Why are those discussion misinformed? Most formal analysis tools
| (Coq, Isabelle, Agda(?)) usually require a proof that a function
| terminates. This is I think is equivalent to proving that it is
| total implying it is primitive recursive?
| bmillwood wrote:
| > This is I think is equivalent to proving that it is total
| implying it is primitive recursive?
|
| No, as the article shows there are functions which terminate
| that aren't primitive recursive, and indeed Agda and
| (probably?) the others can prove termination for some (but
| necessarily not all) terminating non-primitive-recursive
| functions.
|
| I think the misinformation that the article is complaining
| about is something like (my paraphrase):
|
| > "Turing completeness" means "can do computation" while "non-
| Turing complete" means both "can't do computation" and "has
| nice configuration-language properties"
|
| The article points out:
|
| - you can be non-Turing complete and still do lots of
| computationally-expensive / tricky work
|
| - your configuration language probably wants much stricter
| limits than merely being non-Turing complete
| chowells wrote:
| > I think the misinformation that the article is complaining
| about is something like (my paraphrase):
|
| > > "Turing completeness" means "can do computation" while
| "non-Turing complete" means both "can't do computation" and
| "has nice configuration-language properties"
|
| "Turing complete" means it can do _any_ computation a Turing
| machine can. That is absolutely more power than is desired
| about 99.99% of the time. You almost always want your
| algorithms to contain no infinite loops.
|
| (Algorithms. Not IO loops. Those are different, and the
| process of taking outside input while the program is running
| is outside the scope of what a Turing machine talks about
| anyway.)
|
| Turing completeness is an ergonomics hack, and one with a
| decently successful history. But it's no panacea, and if we
| could find an ergonomic way to get rid of it, that would be a
| win.
|
| Yes, even if we didn't also enforce primitive recursion.
| Sure, it's nice to know you're also not accidentally running
| Ackerman's function, but to be honest... I've had many more
| accidental infinite loops than accidental Ackerman's
| functions in my code. By approximately 10,000 to 0.
|
| No system can ever prevent all errors. So let's focus on
| preventing the most common current ones.
| nine_k wrote:
| Possibly there are more ways to be non-Turing-complete than
| being a nice total terminating function. For instance, an
| infinite loop is neither capable of universal computation nor
| is terminating.
| IshKebab wrote:
| I haven't got to the end of it but I assume this was motivated
| by some configuration languages using "not Turing complete" as
| a feature, when the feature they _really_ want to advertise is
| "reasonably bounded execution time".
|
| It came up recently in this discussion about CEL:
|
| https://news.ycombinator.com/item?id=40954652
| nyrikki wrote:
| As you are talking about formal proofs, and not the scientific
| counterexamples modern programming uses:
|
| Proving a function is total in the general case is a NP total
| search problem.
|
| IIRC this is equivalent to NP with a co-NP oracle, or the
| second level on the PH hierarchy, aka expensive if even
| possible even in many small problems.
|
| Most of those tools work best if you structure your programs to
| be total, of which structural programing with only FOR or
| iteration count limited WHILE/recursion are some the most
| common methods.
|
| While just related to SAT, look at the tractable forms of
| Schaefer's dichotomy theorem is the most accessible lens I can
| think of.
| BalinKing wrote:
| > Proving a function is total in the general case is a NP
| total search problem.
|
| My intuition suggests this should be undecidable--could you
| elaborate on the difference between this and the halting
| problem?
| nyrikki wrote:
| Halt is a decision problem, TFNP is a combinatorial problem
| constructed of decision problems.
|
| The HALT decider is a total Turing machine that represents
| a total function.
|
| I am struggling to explain this in a rigorous fashion, and
| there are many open problems.
|
| NP is where the answer "yes" is verifiable in polynomial
| time.
|
| co-NP is where the answer "no" is verifiable in polynomial
| time.
|
| NP is equivalent to second order predicts logic where the
| second term is existential 'there exists..'
|
| co-NP is equivalent to second order predicts logic where
| the second term is universal 'for any'
|
| We know P=co-P, or that the yes and no answers are both
| truthy.
|
| We think that NP!=co-NP
|
| Many useful problems are semi-decidable or recursively
| enumerable.
|
| Determining if a computable function is total is not semi-
| decidable.
|
| It is the subtle difference between proving a TM halts for
| any input vs halts for each input.
|
| Termination analysis is the field of trying to figure out
| if it halts for each input. It is actually harder than
| HALT, being on the second level of PH on the co-NP side.
|
| If that granularity isn't important to you, I personally
| don't think there is much of a risk in using the decidable
| metric as a lens.
|
| Just remember that something is decidable if and only if
| both it and its complement are semi-decidable.
|
| Semi-decidable problems often have practical applications
| even without resorting to approximations etc ...
| ykonstant wrote:
| The conclusion to the article has some pretty good points
| regarding configuration languages; I wonder if any present
| language satisfies all or most of those points.
| nine_k wrote:
| Let's pick Dhall and see if it fails any of the points. It
| seems closest.
| talideon wrote:
| Skylark also. It's essentially Python with anything more than
| primitive recursive functions cut out.
| extrabajs wrote:
| One point that the article is trying to make is that even
| something in PRF can give rise to a very long-running
| computation.
| nyrikki wrote:
| While imperative, and not 'pure' even C was created to set
| upper bound of the number of iterations of every loop being
| known before entering, thus PR
|
| Dennis Ritchie's research at MIT was focused on what he called
| loop programming.
|
| The complexity of loop programs - ALBERT R. MEYER and DENNIS M.
| RITCHIE
|
| https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
|
| Structured programming, the paradigm that almost every modern
| programmer follows by default is really pushing you to
| primitive recursive functions.
|
| That almost universal acceptance of structured programming
| compared to the other two types, pop and functional, is why
| people are confused about Dykstra's goto is harmful paper.
|
| While primitive recursive functions don't contain the entire
| set of computable functions, they do contain almost all
| intuitive ones that are guaranteed to HALT (total).
|
| Unfortunately there are some real needs for languages to
| support loops that have an indeterminate number of iterations
| when you enter the loop, but it is a foot gun that is avoidable
| by only using them when required.
|
| Even COBOL was modernized with unrestricted goto being moved to
| the ALTER command.
|
| I can't think of a modern, useful language that doesn't allow
| for PR functions.
|
| But even in C, if you avoid 'while', explicitly avoid fall
| through, etc... you will produce code that almost always is a
| total functions that will always HALT.
|
| There are cases like even type inference in ML, which is
| pathological in that it is way cheaper than the complexity
| class, thus worth the risk, despite not being total functions
| that make it hard for a language to restrict those use cases.
|
| So I would say that with a pragmatic approach, all languages
| support defaults that support most of the points, but imposed
| constraints that enforce them would seriously constrain the
| utility of the language.
|
| If you review even the hated SOLID and Clean frameworks,
| they're pushing you towards this model too IMHO.
|
| I think the universal acceptance of structured programming,
| makes this easy to forget or even fail to teach. But as an old
| neck beard, we were taught the risks of WHILE etc...
| 4ad wrote:
| I am a CUE developer. CUE is primitive recursive. It also happens
| to fulfill your desired criteria for a "good" configuration
| language.
| 4ad wrote:
| For fun, here is CUE simulating an arbitrary but finite number
| of steps of Rule 110[0]:
| https://cuelang.org/play/?id=Ityqia88Mvq#w=function&i=cue&f=...
|
| [0] https://en.wikipedia.org/wiki/Rule_110
___________________________________________________________________
(page generated 2024-08-03 23:00 UTC)