coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vincent Aravantinos <vincent.aravantinos AT yahoo.fr>
- To: "Jimmy Miller" <captainthunder AT gmail.com>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Factorial function
- Date: Tue, 11 Sep 2007 15:14:42 +0200
- Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.fr; h=Received:X-YMail-OSG:In-Reply-To:References:Mime-Version:Content-Type:Message-Id:Cc:Content-Transfer-Encoding:From:Subject:Date:To:X-Mailer; b=ypsFI7dPvYoH0iSfJ+Nv6wmYL/2LG6kdeu025r2z138iw0Kw/IoKCHlluABWJUvSIo0Iv9AAcmJxkZCXwgeCfuLw4SmzF8H/7RybP4qtmf6npzKZWjIOCwe5EW92Fs5bvLROXwyNA4NOTUWQCghrBp5Cq5T5rcM2AAbhpIOuilA= ;
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Le 3 sept. 07 à 17:39, Jimmy Miller a écrit :
In Coq.Arith.Factorial, the fact function is defined as follows:
Fixpoint fact (n:nat) : nat :=
match n with
| O => 1
| S n => S n * fact n
end.
I think this is equivalent to this :
Fixpoint fact (p:nat) : nat :=
match p with
| O => 1
| S n => S n * fact n
end.
ie. the parameter n is not the same as the n bounded in the second branch of the match. Thus 'fact' is indeed seeing its parameter decreasing.
But I'm having trouble understanding how this function works. Usually
in a recursive factorial, fact is given n-1 each time it recurses, but
here I only see n getting passed to it. Wouldn't this cause infinite
recursion, because fact gets the same argument every time, and thus n
will never reach 0?
Vincent
- [Coq-Club] Factorial function, Jimmy Miller
- Re: [Coq-Club] Factorial function, Vincent Aravantinos
- Re: [Coq-Club] Factorial function, Adam James Chlipala
Archive powered by MhonArc 2.6.16.