Zombie (programming language)

[Philip Thrift]

We propose a full-spectrum dependently typed programming language, Zombie, which supports general recursion natively. ... Zombie also features an optional termination-checker, allowing nonterminating programs returning proofs as well as external proofs about programs.

Vilhelm Sjöberg - https://www.cs.yale.edu/homes/vilhelm/

Stephanie Weirich - https://www.seas.upenn.edu/~sweirich/

https://www.cis.upenn.edu/~sweirich/papers/sjoberg-thesis.pdf

@philipthrift

[Brent Meeker]

What does "general recursion" mean?  Is recursion in LISP not "general"?

Brent

--
You received this message because you are subscribed to the Google Groups "Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email to everything-li...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/f547910f-4e56-45a1-b7ff-eaa05b7f2f30o%40googlegroups.com.

[Philip Thrift]

Programmers use 'general' to contrast with 'primitive'.

general:

In mathematical logic and computer science, a general recursive function (often shortened to recursive function) or μ-recursive function, is a partial function from natural numbers to natural numbers that is "computable" in an intuitive sense. 

In computability theory, it is shown that the μ-recursive functions are precisely the functions that can be computed by Turing machines (this is one of the theorems that supports the Church–Turing thesis). The μ-recursive functions are closely related to primitive recursive functions, and their inductive definition (below) builds upon that of the primitive recursive functions. However, not every μ-recursive function is a primitive recursive function—the most famous example is the Ackermann function

primitive:

https://mathworld.wolfram.com/PrimitiveRecursiveFunction.html

As first shown by Meyer and Ritchie (1967), do-loops (which have a fixed iteration limit) are a special case of while-loops. A function that can be implemented using only do-loops is called primitive recursive. (In contrast, a computable function can be coded using a combination of for- and while-loops, or while-loops only.) Examples of primitive recursive functions include power, greatest common divisor, and (the function giving the th prime).

The Ackermann function is the simplest example of a well-defined total function that is computable but not primitive recursive, providing a counterexample to the belief in the early 1900s that every computable function was also primitive recursive.

code in various programming languages:

The Ackermann function is a classic example of a recursive function, notable especially because it is not a primitive recursive function. 

https://rosettacode.org/wiki/Ackermann_function

@philipthrift

On Wednesday, June 10, 2020 at 5:31:39 PM UTC-5, Brent wrote:

What does "general recursion" mean?  Is recursion in LISP not "general"?

Brent

On 6/10/2020 12:08 PM, Philip Thrift wrote:

We propose a full-spectrum dependently typed programming language, Zombie, which supports general recursion natively. ... Zombie also features an optional termination-checker, allowing nonterminating programs returning proofs as well as external proofs about programs.

Vilhelm Sjöberg - https://www.cs.yale.edu/homes/vilhelm/

Stephanie Weirich - https://www.seas.upenn.edu/~sweirich/

https://www.cis.upenn.edu/~sweirich/papers/sjoberg-thesis.pdf

@philipthrift

--
You received this message because you are subscribed to the Google Groups "Everything List" group.

To unsubscribe from this group and stop receiving emails from it, send an email to everyth...@googlegroups.com.

[Bruno Marchal]

On 11 Jun 2020, at 00:31, 'Brent Meeker' via Everything List <everyth...@googlegroups.com> wrote:

What does "general recursion" mean?  Is recursion in LISP not "general”?

This is an abandoned expression for partial recursive function (they are the programmable function, total or not). It is the phi_i.

Gödel use “recursive function” for what we call now “primitive recursive function”, which is a subset of total computable function, which when closed for the MU operator gives all partial computable function. I almost never use the “primitive recursive function”, here. I did it when I showed the Turing completes of the combinators, though.

The primitive recursive functions can be replaced by much elementary functions (Smullyan did that), or even by diophantine polynomial  relations (but that is rather long to prove, and not so easy).

Bruno

To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/4cc42076-4927-b8da-e0e9-2f62d73a3676%40verizon.net.