TLAPS and primitive-recursive functions

[Andrew Helwer]

I've been enjoying playing around with TLAPS over the holidays, with the intention of writing a Wikipedia article if I find enough material to work with. I'm impressed with the ability of the SMT solver to prove theorems of arithmetic, but have run into a wall when trying to prove theorems requiring primitive-recursive function definitions.

Let's consider a simple primitive-recursive function, which sums all the elements of a set of numbers in Nat:

SetSumV0[S \in SUBSET Nat] ==

IF S = {} THEN 0

ELSE LET e == CHOOSE val \in S : TRUE IN

e + SetSumV0[S \ {e}] 

TLAPS fails to prove this base case theorem:

THEOREM SetSumV0BaseCase == SetSumV0[{}] = 0

 BY DEF SetSumV0

Although strangely, if we rewrite SetSum as an operator TLAPS has more success:

SetSumV1(S) ==

 LET SS[T \in SUBSET S] ==

IF T = {} THEN 0

ELSE LET e == CHOOSE val \in T : TRUE IN

e + SS[T \ {e}]

IN SS[S]

THEOREM SetSumV1BaseCase == SetSumV1({}) = 0

BY DEF SetSumV1

Q1) Why does TLAPS find SetSumV1 easier to analyze than SetSumV0? Is it because SetSumV1 drops the dependency on Nat?

TLAPS is unable to prove this theorem about SetSumV1:

THEOREM SetSumV1Test == SetSumV1({2}) = 2

BY DEF SetSumV1

I understand this isn't a very useful theorem to prove, but we also run into a wall trying to prove more general statements quantifying over the Natural numbers so this seems a good place to start.

Q2) Is there a way for me to give TLAPS more information about how SetSumV1 works without introducing axioms and assumptions beyond the literal text of the function itself? What information can TLAPS extract from this primitive-recursive function?

Thanks!

Andrew

 

 

 

 

 

 

 

 

[Stephan Merz]

Hi Andrew,

I'm afraid your example is more complicated than it looks at first sight. I would expect to be able to prove theorems about your function only when the argument set is finite, and in that sense your second definition may be easier to work with.

Most importantly, you want to prove the following theorem:

LEMMA SetSumDefined ==

  ASSUME NEW S \in SUBSET Nat, IsFiniteSet(S)

  PROVE  SetSum(S) = [T \in SUBSET S |-> IF T = {} THEN 0 ELSE ...]

This is not obvious because a TLA+ function definition

f[x \in S] == exp

is really shorthand for

f == CHOOSE f : f = [x \in S |-> exp]

and as with any CHOOSE expression, you have to show that a suitable value (here, function) exists. There is some library support for carrying out the required proofs: you want to EXTEND module WellFoundedInduction and use lemma WFInductiveDefLemma, which requires proving several hypotheses. (The last hypothesis is trivial if you remember the expansion explained above.) Most importantly, you need to prove that the subset order is well-founded over subsets of the finite set S introduced in the hypothesis of lemma SetSumDefined. The necessary infrastructure ought to be in place, though I'd be interested in hearing if you run into problems.

I'd suggest that you start with a simpler recursive function definition over natural numbers as a warm-up exercise. Look at module NaturalsInduction, which has the required helper lemmas. At the bottom of the module you'll find an example of how these lemmas are applied for the definition of the factorial function.

Regards,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Roy Overbeek]

Dear Stephan,

I am now trying to understand how to prove statements of the form f[x] = y, where f is a recursively defined function. Your suggestion to consider a simple definition is helpful. However, given:

----

factorial[n \in Nat] == IF n = 0 THEN 1 ELSE n * factorial[n-1]

THEOREM FactorialDefConclusion == NatInductiveDefConclusion(factorial, 1, LAMBDA v,n : n*v)

<1>1. NatInductiveDefHypothesis(factorial, 1, LAMBDA v,n : n*v)

  BY DEF NatInductiveDefHypothesis, factorial 

<1>2. QED

  BY <1>1, NatInductiveDef

THEOREM FactorialDef == \A n \in Nat : factorial[n] = IF n = 0 THEN 1 ELSE n * factorial[n-1]

  BY FactorialDefConclusion DEFS NatInductiveDefConclusion 

----

I already struggle to prove factorial[0] = 0. Am I overlooking something trivial?

Kind regards,

Roy

Op zondag 25 december 2016 09:19:50 UTC+1 schreef Stephan Merz:

[Stephan Merz]

Hi,

maybe you have better success in proving that factorial[0] = 1?

LEMMA factorial[0] = 1

BY FactorialDef

Regards,

Stephan

[Roy Overbeek]

...thanks, next time I'll be sure to take a rest before I write.

Op dinsdag 23 januari 2018 17:17:01 UTC+1 schreef Stephan Merz: