40 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
0
votes
1
answer
106
views
In Standard ML, are datatype constructors considered values?
My working definition for value is a special kind of expression that evaluates to itself. So 1 is a value, and 1 + 1 is valuable but not a value because it evaluates to 2.
A datatype constructor like ...
1
vote
0
answers
89
views
Why is `Prelude.mod` a total function?
Why is Prelude.mod marked as a total function when it is not defined when the second argument is zero?
Main> :total mod
Prelude.Num.mod is total
I was just bit by this and ran into a run-time ...
3
votes
1
answer
256
views
Idris totality check
I am compiling the following simple program using Idris2.
import Data.Fin
%default total
negate : {k:_} -> Fin k -> Fin k
subt : {k:_} -> Fin k -> Fin k -> Fin k
add : {k:_} -> Fin ...
0
votes
1
answer
42
views
How to crash on internal bug and force totality
I'm ffi-ing to C and the function I call returns an int to mean gt, eq or lt. I want to crash on anything other than 1, 0 or -1 cos that should never happen. And I'd like Idris to consider 0, 1 and -1 ...
joel's user avatar
- 8,132
1
vote
0
answers
184
views
Why is this Idris function not total and what could be done to make it check total?
This Idris function does not successfully check for totality, however in my mind it seems that all cases are covered. This is my merge function in a merge sort.
Using Idris version 1.3.3
Error.
*d:/...
Phil's user avatar
- 50.9k
3
votes
1
answer
477
views
Can any additional axiom make Coq Turing complete?
Here I mean axiom as what we can define with the Axiom keyword in Coq Gallina, not with such command-line argument passing to Coq.
I know some axioms make Coq inconsistent. However, AFAIK they don't ...
0
votes
1
answer
96
views
Can I avoid explicitly discharging invalid cases in total functions in Idris?
Consider the following (very simplified) example of constraining a datatype via a side-condition on its values:
data Transport = Car | Foot | Boat
total wheels : (transport : Transport) -> {auto ...
6
votes
4
answers
413
views
Defining recursive function over product type
I'm trying to formalize each integer as an equivalence class of pairs of natural numbers, where the first component is the positive part, and the second component is the negative part.
Definition ...
2
votes
1
answer
291
views
Convince Idris about recursive call totality
I have written the following type to encode all possible rational numbers in it:
data Number : Type where
PosN : Nat -> Number
Zero : Number
NegN : Nat -> Number
Ratio : Number -...
2
votes
0
answers
148
views
totality checking with indirect mutually recursive datatypes in Idris
I am working with an abstract syntax tree, where I'd like to give the binders their own type. This seems to cause problems for Idris's totality checking...
With a typical self-referencial Tree Idris ...
1
vote
1
answer
266
views
Proving totality of a function taking at most n recursive calls
Let's say we're writing an implementation of a lambda calculus, and as a part of that we'd like to be able to choose a fresh non-clashing name:
record Ctx where
constructor MkCtx
bindings : List ...
5
votes
1
answer
572
views
Coq can't compute well-founded defined with Fix, but can if defined with Program Fixpoint
As an exercise to understand recursion by a well-founded relation I decided to implement the extended euclidean algorithm.
The extended euclidean algorithm works on integers, so I need some
well-...
0
votes
2
answers
232
views
Cannot determine termination
Function for determining if a set is a subset of another:
Fixpoint subset (s1:bag) (s2:bag) : bool :=
match s1 with
| nil => true
| h :: t => match (beq_nat (count h s1) (count h s2)) ...
7
votes
2
answers
2k
views
Teach coq to check termination
Coq, unlike many others, accepts an optional explicit parameter,which can be used to indicate the decreasing structure of a fixpoint definition.
From Gallina specification, 1.3.4,
Fixpoint ident ...
2
votes
1
answer
325
views
Finding a well founded relation to prove termination of a function that stops decreasing at some point
Suppose we have:
Require Import ZArith Program.
Program Fixpoint range (from to : Z) {measure f R} : list :=
if from <? to
then from :: range (from + 1) to
else [].
I'd like to convince ...