4 ms·

That's a bit different, isn't it? As agda is total, and requires everything be proved to halt. Whereas the context here is a complete language, where you do n

That's a bit different, isn't it? As agda is total, and requires everything be proved to halt. Whereas the context here is a complete language, where you do not get such strong properties, but must still try to reason anyway. I didn't discuss any specific ways to infer termination or nontermination (though I definitely think those are interesting too!), only a broad strategy for reasoning about them.

chriswarbo 4y ago
> As agda is total, and requires everything be proved to halt. Not quite; everything in Agda must either terminate or co-terminate. We can use co-termination to represent general recursion, e.g. using Delay: data Delay : Type -> Type where Now : {t: Type} -> t -> Delay t Later : {t: Type} -> Delay t -> Delay t It's trivial to write any program using Delay, e.g. if we have a function 'step: TuringMachine -> TuringMachine' which performs one step of any Turing machine, we can run any TuringMachine using: run : TuringMachine -> Delay TuringMachine run thisState = case thisState == nextState of true -> Now thisState -- We've entered a halting state false -> Later (run nextState) where nextState = step thisState This is similar to "infinite lists" in lazy languages (like Haskell); e.g. if we call 'run' with a non-halting TuringMachine, we'll get 'Later (Later (Later (...)))'
- cvoss 4y ago
  But I mean, 'run' is a total function and it does halt. When you call 'run' on your non-halting TuringMachine, the language interpreter reduces exactly one call to 'step' and then terminates with the result 'Later <an unevaluated expression>'. Further computation only occurs if and when you pump the 'Later ...' value for further terms, and that can happen only finitely many times because repeated pumping can only come from a standard recursion, ultimately, which is terminating.
- SkySkimmer 4y ago
  Did HN eat the delay symbol? I don't think a regular "data" would work for this. https://agda.readthedocs.io/en/v2.6.3/language/coinduction.html#old-coinduction https://agda.readthedocs.io/en/v2.6.3/language/coinduction.h...
  - chriswarbo 4y ago
    Oops, yeah; I know Agda needs special handling for codata (co-patterns, sharp/flat, etc.) Ironically, I'm more familiar with using codata in Coq; even though it's notoriously under-supported (breaking subject-reduction, no alternative to cofix, etc.)
- deleted 4y ago
  [deleted]
- hgsgm 4y ago
  Lists have a consumable head. What you constructed looks like a left fold, a stack of wrappers with the data buried at the bottom.
  - chriswarbo 4y ago
    > a stack of wrappers with the data buried at the bottom Yes, 'Delay t' stores a value "at the end" (in the 'Now' constructor), but doesn't store anything "on the way" (in the 'Later' constructor). In contrast, 'List t' stores values "on the way" (in Cons), but doesn't store anything "at the end" (in Nil). Another useful example is (Peano) natural numbers, which don't store any values "at the end" (Zero) or "on the way" (Successor). Natural numbers are isomorphic to 'List ()' and 'Delay ()' (whose 'elements' contain no information) > Lists have a consumable head Slight nit-pick: only non-empty lists have a head. Non-empty lists are isomorphic to '(t, List t)'. Consuming the head of a 'Delay t' is still useful, since they act like a counter; or (equivalently) as a notion of logical time. I find this stuff fascinating, and explored it in more detail at http://www.chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://www.chriswarbo.net/blog/2014-12-04-Nat_like_types.htm...

chriswarbo 4y ago

> As agda is total, and requires everything be proved to halt. Not quite; everything in Agda must either terminate or co-terminate. We can use co-termination to represent general recursion, e.g. using Delay: data Delay : Type -> Type where Now : {t: Type} -> t -> Delay t Later : {t: Type} -> Delay t -> Delay t It's trivial to write any program using Delay, e.g. if we have a function 'step: TuringMachine -> TuringMachine' which performs one step of any Turing machine, we can run any TuringMachine using: run : TuringMachine -> Delay TuringMachine run thisState = case thisState == nextState of true -> Now thisState -- We've entered a halting state false -> Later (run nextState) where nextState = step thisState This is similar to "infinite lists" in lazy languages (like Haskell); e.g. if we call 'run' with a non-halting TuringMachine, we'll get 'Later (Later (Later (...)))'

cvoss 4y ago
But I mean, 'run' is a total function and it does halt. When you call 'run' on your non-halting TuringMachine, the language interpreter reduces exactly one call to 'step' and then terminates with the result 'Later <an unevaluated expression>'. Further computation only occurs if and when you pump the 'Later ...' value for further terms, and that can happen only finitely many times because repeated pumping can only come from a standard recursion, ultimately, which is terminating.
SkySkimmer 4y ago
Did HN eat the delay symbol? I don't think a regular "data" would work for this. https://agda.readthedocs.io/en/v2.6.3/language/coinduction.html#old-coinduction https://agda.readthedocs.io/en/v2.6.3/language/coinduction.h...
- chriswarbo 4y ago
  Oops, yeah; I know Agda needs special handling for codata (co-patterns, sharp/flat, etc.) Ironically, I'm more familiar with using codata in Coq; even though it's notoriously under-supported (breaking subject-reduction, no alternative to cofix, etc.)
deleted 4y ago
[deleted]
hgsgm 4y ago
Lists have a consumable head. What you constructed looks like a left fold, a stack of wrappers with the data buried at the bottom.
- chriswarbo 4y ago
  > a stack of wrappers with the data buried at the bottom Yes, 'Delay t' stores a value "at the end" (in the 'Now' constructor), but doesn't store anything "on the way" (in the 'Later' constructor). In contrast, 'List t' stores values "on the way" (in Cons), but doesn't store anything "at the end" (in Nil). Another useful example is (Peano) natural numbers, which don't store any values "at the end" (Zero) or "on the way" (Successor). Natural numbers are isomorphic to 'List ()' and 'Delay ()' (whose 'elements' contain no information) > Lists have a consumable head Slight nit-pick: only non-empty lists have a head. Non-empty lists are isomorphic to '(t, List t)'. Consuming the head of a 'Delay t' is still useful, since they act like a counter; or (equivalently) as a notion of logical time. I find this stuff fascinating, and explored it in more detail at http://www.chriswarbo.net/blog/2014-12-04-Nat_like_types.html http://www.chriswarbo.net/blog/2014-12-04-Nat_like_types.htm...