Skip to main content

Questions tagged [total]

A total function is defined on all inputs and always terminates. Contrast with partial functions.

Filter by
Sorted by
Tagged with
6 votes
2 answers

Possible root cause(s) of the misunderstanding that DTT implies not Turing complete?

I myself have fallen prey to this misconception, i.e., that being dependently typed as in Agda, Coq, etc., implies not being Turing complete, which can be (whether now or previously) found at quite a ...
Municipal-Chinook-7's user avatar
18 votes
1 answer

How can all functions be total in Isabelle?

Isabelle/HOL’s logic is called a logic of “total functions”, yet there are functions that are obviously not total, such as division div. How does this make sense?
Joachim Breitner's user avatar