14
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 useful to keep them apart. I will focus on the former.
The ability of a
programming languages to represent, manipulate (and run) its programs
as data goes ...
14
@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$ times, to get $$f(n) = 2f(n - \log n) + f(n - \log n - 1) + \ldots + f(n - 2 \log n) \ge \log n \cdot f(n - \log n) \ .$$
Use this inequality $n / \log n$ times, ...
12
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 appear at the third level of the Grzegorczyk hierarchy.
PR can alternatively be defined using the iteration function in place of recursion.
A good reference for ...
12
Is it possible to make a "smart" trampoline function that takes two forms of a function, a trampolined version and a non-trampolined version, and chooses (or predicts) the most efficient strategy?*
Yes, it's possible to do things like this, but if you control the compiler, it's usually faster and easier to do something else. The main exception is when you ...
9
If you want to include a fixpoint combinator in the language, you don't need to change anything to the syntax of types or the rules to type existing expressions. All it takes is adding one constant, a rule to type it and a rule to reduce expressions containing it:
$$
\dfrac{}{\mathsf{fix} : (\tau \rightarrow \tau) \rightarrow \tau} \qquad
\mathsf{fix} \, ...
answered Mar 30 '14 at 14:00
Gilles 'SO- stop being evil'
2,5271 gold badge23 silver badges33 bronze badges
8
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 runtime,” then it is in P. There is a tally language in E∖P by a standard diagonalization argument.
Is there a problem which can be solved in time $f(n)$, but ...
7
Is that the technical term referring to productive sets and creative sets, or is it just a manner of speaking?
Neither, actually -- it's a different technical term.
The type of streams of natural numbers can be interpreted as the final coalgebra for the functor $F(X) \triangleq \mathbb{N} \times X$. That is, define the category of $F$-algebras as follows:
...
7
Productive here just means that it isn't stuck.
An unorthodox (seemingly impredicative ) formulation of the sieve of Eratosthenes is
S = {n : n ∈ N, n > 1} \ ⋃p ∈ S { p q : q ∈ N, q ≥ p }
The following code is stuck, reflecting the above definition more or less verbatim:
primes = gaps 2 $ foldr (\p r-> ...
6
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 "natural" recursion principles on Scott numerals, and because they correspond to recursors in this encoding, they are guaranteed to terminate.
However, if you want ...
6
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 Vrech, 2008
The problem of typing polymorphic recursion (i.e., recursive function
definitions rec {x = e} where different occurrences of x in e are used
...
6
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 programming language that you have as small as possible so that when you enter the system and start to make it interpret itself it will work. So therefore you want a ...
5
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 Schmidhuber that solves problems in an optimal way. It uses a
recursive self-improvement protocol in which it rewrites its own code
when it can prove the new ...
5
I think my comment was a little cryptic, so let me unpack. The key intuition behind hylomorphisms is that they let you reify the call graph as a data structure. You unfold a datastructure to build a representation of the call graph, and then you fold over the intermediate structure to consume and finish the computation.
Lists are a little misleading, ...
4
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-conversion is part of the equational theory of the lambda-calculus, this has no effect on the semantics of the program.
Furthermore, in the lambda calculus, all of ...
4
A context-free grammar is cyclic if there exists a non-terminal $A$ and a derivation in one or more steps $A\Rightarrow^+ A$. It is left-recursive if there exists a non-terminal $A$, a mixed sequence of terminals and non-terminals $\gamma$, and a derivation in one or more steps $A\Rightarrow^+ A\gamma$.
Hence cyclic implies left-recursive, but the converse ...
4
What Sam said.
Also, it's really well under a page. If you're familiar with evaluation contexts, you can specify the call-by-value lambda calculus like this:
Terms
$$M ::= x \mid (M \, M) \mid (\lambda x . M)$$
Values
$$V = (\lambda x . M)$$
Evaluation contexts
$$E ::= [\:] \mid ([\:] M) | (V [\:])$$
The (only) reduction rule:
$$E[((\lambda x . M) ...
3
This paper by Jurgen Schmidthuber might be of interest:
http://arxiv.org/pdf/cs/0309048.pdf
3
All you really need is the definition of the untyped $\lambda$-calculus, which you can find in numerous places. Everything else follows from that.
3
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 natural number. In logic, recursion appears in Skolem [1923], where it is noted that many basic functions can be defined by simple applications of the method. The ...
3
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.
3
(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 extensions of System F with (co)inductive types (among other things). In the first part of the paper we define a strongly-normalizing language that can deal ...
2
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 embed $A$ as $M_{32}^{th}$ block of a $3n \times 3n$ matrix $M$ with rest of the blocks all zero matrices. Similarly, I can embed $B$ as $N_{21}^{th}$ block of $3n ...
2
... 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$ exists for arbitrary $\alpha$.
Indirect left recursion exists when there's a rule $A \to^* A\alpha$ for arbitrary $\alpha$. Note the star, implying possibly many ...
2
Your predd2 is not a fixpoint; you could replace the Fixpoint by Definition. And the fact that they are not convertible is due to the lack of eta-conversion for inductive types in Coq.
The reason for this is that we want the conversion to be decidable, and it's already hard to decide beta-eta-conversion in the simply typed case (see Deciding equivalence ...
2
There's a good chance this question is independent of ZFC for most programming languages. In particular, I'd expect it to be true of any language where the shortest Quine is longer than the Kolmogorov complexity decidability bound, the integer $n$ such that no string can be proven to have Kolmogorov complexity $> n$. I don't know to prove this, since ...
1
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 of $1$ rather than $0$, this recurrence is dominated term-by-term by the recurrence
$$U(n)=nU(\frac{n}{2}).$$
For the lower bound, note that it dominates the ...
1
A super quine exists in any language where some n-quines exist: just take the smallest program among all n-quines. I guess you wanted to ask another question.
a k-quine is also always a (kn)-quine for any $n$, so the smallest super quine is a super n-quine for infinitely many n
in any "acceptable programming language" we can prove that for all n, there ...
Only top voted, non community-wiki answers of a minimum length are eligible
