All Questions

Tagged with
Filter by
Sorted by
Tagged with
2
votes
0answers
188 views

Recursive definitions, How it is done?

I read that recursive definitions, refer to the definition of a function in that function body, cannot be done in $\lambda$-calculus, but recursion can be achieved by using $Y$ combinator. As I know, ...
13
votes
1answer
2k views

Is this a generic way to convert any recursive procedure to tail-recursion?

It seems that I've found a generic way to convert any recursive procedure to tail-recursion: Define a helper sub-procedure with an extra "result" parameter. Apply what would be applied to the ...
2
votes
1answer
116 views

Undecidable definition of pure function?

I am trying to come up with a formal definition for functional purity in a simple programming language (think JavaScript). What I've got so far is this: DEFINITION: A statement is impure if ...
15
votes
2answers
864 views

Does the Y combinator contradict the Curry-Howard correspondence?

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
0
votes
2answers
90 views

Recursive equations vs. inference rules

It seems to me that recursive equations can always be presented as inference rules. For the forward direction, an example is addition over Peono numerals (built from $O$ and $S(\_)$) $$ \begin{align}...
6
votes
1answer
354 views

Inductive vs. recursive definition

When should I call a definition recursive and when should I call it inductive? I have read Carl Mummert's nice answer on MSE. So if I understand correctly we refer to definitions of objects like ...
20
votes
2answers
2k views

Recursive definitions over an inductive type with nested components

Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to ...