15 votes
Accepted

Program reasoning about own source code

I think you are asking about two different things. The ability of a programming language to represent all its programs as data. Reasoning about programs as data. For analytical purposes it's ...
user avatar
14 votes
Accepted

Solve the recurrence $f(n) = f(n-1) + f(n - \log n)$

@Chandra, @Emil, and myself solved the question in the comments. The solution is $$f(n) = 2^{\Theta(n \log \log n / \log n)} \ .$$ To see the lower bound, apply the recurrence definition $\log n$ ...
user avatar
  • 1,101
12 votes
Accepted

Growth rate of primitive recursive functions

The answer is no, there is no exponential bound on PR. PR contains Knuth's up-arrow functions, Elementary functions, etc. PR is equal to the union of Grzegorczyk hierarchy. Exponential functions ...
user avatar
  • 21.3k
8 votes
Accepted

Are there problems for which divide-and-conquer / recursion is provably useless?

Is there a problem with an exponential algorithm which has no algorithm with polynomial recursive runtime? Yes. Note that if a tally language has “recursive algorithm” with polynomial “recursive ...
user avatar
  • 16.3k
7 votes

Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

You should have a look at the following paper -- and the previous work by Gori and Levi: On Polymorphic Recursion, Type Systems, and Abstract Interpretation Marco Comini, Ferruccio Damiani, Samuel ...
user avatar
  • 1,910
6 votes
Accepted

Termination checking for Scott-encodings in System F with positive-recursive types

I'll first point you to Types for the Scott Numerals by Plotkin, Cardelli and Abadi, where they show how to encode Scott numerals in plain old system F. This at least shows that you can write the "...
user avatar
  • 13.2k
6 votes

Program reasoning about own source code

No there is no current system that does all four steps in your system. If you want to design a system one of the first requirements is homoiconic language. At minimum you would want your core ...
user avatar
5 votes

Program reasoning about own source code

As @user217281728's answer mentions there are a type of machines related more to inference and AI, called Gödel Machines A Gödel machine is a self-improving computer program invented by Jürgen ...
user avatar
  • 571
4 votes

What is the relationship between tail recursion with other recursions?

From the point of view of lambda-calculus "tail call optimization" means take a CPS converted version the program, and eta-reduce continuations of the form $\lambda x. k\;x$ to $k$ Since eta-...
user avatar
3 votes

Termination checking for Scott-encodings in System F with positive-recursive types

(Sorry for the blatant self-advertisement that follows!) In addition to what was already said, you should really check out our recent TOPLAS paper (https://doi.org/10.1145/3285955), which deals with ...
user avatar
3 votes

History of recursion

From Recursive Functions article on SEP: The use of recursion goes back to the 19th century. Dedekind [1888] used the notion to obtain functions needed in his formal analysis of the concept of ...
user avatar
  • 21.3k
3 votes

History of recursion

Maybe slightly tangential to the original question, but the blog entry "How recursion got into programming: a comedy of errors" describes an interesting part of early computing history.
user avatar
3 votes

Program reasoning about own source code

This paper by Jurgen Schmidthuber might be of interest: http://arxiv.org/pdf/cs/0309048.pdf
user avatar
3 votes

Reference for automatically deriving dynamic programming algorithms from recursive algorithms?

There's actually two questions here! The transformation you ask about is called the tupling transformation. Basically, if your recursive calls follow a fixed pattern of overlap, a memo-table can be ...
user avatar
3 votes
Accepted

Linear regression as a hylomorphism

You can indeed see linear regression as arising from a fixed point computation, but it is better to think of it as related to transitive closure computations than to folds or unfolds. Regression is ...
user avatar
3 votes
Accepted

Time complexity for multiplying two lower triangular matrices

With the expert hints of Mr Emil, I could find a reduction of general matrix multiplication to triangular matrix multiplication. If we wish to multiply two $n \times n$ matrices $A$ and $B$, I can ...
user avatar
2 votes
Accepted

Why can a Predictive Parser contain E' -> TE' | ε

... is not valid since we have "left recursion" (a variable that calls itself). That's not what a left recursion is. That's simply recursion. Direct left recursion is when a rule $A \to A\alpha$ ...
user avatar
  • 690
2 votes

Definitional equality of recursive function definition by "infinite unfolding"

Your predd2 is not a fixpoint; you could replace the Fixpoint by Definition. And the fact ...
user avatar
  • 521
1 vote
Accepted

How can I find tight asymptotic bounds for this half-history recurrence relation?

It is $n^{\Theta(\log n)}$, although I'm not sure exactly what the constant in the theta is. For the upper bound (the one you already have), note that, even without the $n^2$ term but with a base case ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible