The Coq mailing list

["William J. Bowman" <wilbowma AT ccs.neu.edu>]

I don’t think that’s the problem. Another model does get stuck on that equality and returns the if statement waiting for an interpretation of “==“. I didn’t expect Program to be efficient, but I do expect it to terminate quickly on this example, without using 20 GB of memory.

I’ll see if I can reduce the other model to something as small.

-- 

Sent from my phoneamajig

On Sep 20, 2019, at 17:35, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Perhaps they forgot to instantiate the atom type?  the computation would get stuck on (x == x'). `Program` often produces humongous functions.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, Sep 20, 2019 at 5:15 PM William J. Bowman <wjb AT williamjbowman.com> wrote:

All,

At the following URL is a model of a language with capture-avoiding substitution
that a student wrote:

  https://gist.github.com/wilbowma/acf125222c64ff715a33b26a0ce8b4ab

The program looks (to me) like it ought to terminate quickly, and it's proven
terminating using Program, yet when we run the substitution function on a small
example... coqtop eats about 20 GB of memory and doesn't terminate within 5
minutes.
I'm using Coq 8.9.1 on MacOS 10.14.2; the same behavior is also observed on
Windows 10.

I'd appreciate any help debugging this.

--
William J. Bowman