coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is Coq SN ?

From: Benoît Viguier <beviguier AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is Coq SN ?
Date: Tue, 1 Mar 2016 05:39:55 +0900
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f169.google.com
Ironport-phdr: 9a23:kQb5ghbBhJYdSanxYGTcXN//LSx+4OfEezUN459isYplN5qZpc+zbnLW6fgltlLVR4KTs6sC0LqJ9f6wEjVbvd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcODKFwT2HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzA8nxxPhRTy0hD1Q5b8qGOuvOdj2SaHPMDsZb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf5qg==

@Jonathan,

For non terminating functions (such as a program interpreter semantic, virtual machine simulations...), We recurse on a kind of fuel.

Fixpoint execution (fuel:nat) (program:state -> state) (s:state) := match fuel with

| 0 => state

| S f => execution f program (program s)

end.

Then you will need to prove that there exist enought fuel to execute fully your program.

Kind regards.

2016-03-01 4:42 GMT+09:00 Jonathan Leivent <jonikelee AT gmail.com>:

Forgive my type-theory naiveté, but shouldn't we want some part of Coq to not be strongly normalizing, so that it is possible to express and reason about non-terminating functions?

-- Jonathan

Re: [Coq-Club] Is Coq SN ?, (continued)