# Tag Info

Accepted

### Composition with recursion in functions between types

(I'm going to try to write an answer for functional programmers, with Haskell-like code.) First, you should know that using higher-order functions, recursive definitions can be turned into fixed-point ...

### 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 ...
• 2,040
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 "...
• 13.9k

### 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 ...

### Extension of primitive recursion, that is as powerful as System-T

If you're just talking about the expressiveness of functions $\mathbb{N}\rightarrow\mathbb{N}$, then you can extend primitive recursion to allowing a recursive call over a Cantor normal form, where ...
• 13.9k
Accepted

### Is any computational complexity question solved by injury priority method except Post problem?

Priority method gets used a lot in computability theory - see some of the later chapters of Soare's book on computability. Buhrman and Torenvliet use a resource-bounded priority method to build an ...
• 37.4k

### 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 ...
• 32.6k

### 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-...
• 32.6k
Accepted

### How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

The surjective pairing rule is really just as written there by Wadler. Andrej's interpretation is correct. What the equation ...
• 206
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 ...
• 32.6k
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 ...
• 141
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$ ...
• 885

### 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 ...
• 556

### What is formal definition of non-deterministic algorithm in context of primitive/general recursion?

You could easily make Kleene's $\mu$-recursive programs nondeterministic. A $\mu$-recursive program consists of a sequence of function symbols, each defined from previous ones by composition, ...
• 851
1 vote

### How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

Is this not just confusion about notation? If the notation (X, y) is used to signify the introduction rule for then it does ...
• 29.2k
1 vote

### Bad Cycles in Interaction Nets

Quoting from the paper: It is possible to define rules which lead to non-terminating computations, [...] but further constraints on nets can ensure that when a sequence of reductions terminates, the ...
• 12.2k
1 vote

### Composition with recursion in functions between types

The theory behind recursion schemes is that algebraic data types are initial algebras. 1. Recursive types and folds The programmer's point of view is that, given a recursive type, ...
• 206

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