[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Andrew Helwer <andrew...@xxxxxxxxx>*Date*: Sat, 24 Dec 2016 14:37:44 -0800 (PST)

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.

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

**Follow-Ups**:**Re: [tlaplus] TLAPS and primitive-recursive functions***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] About single process system, fairness, and depth-first search option** - Next by Date:
**Re: [tlaplus] TLAPS and primitive-recursive functions** - Previous by thread:
**Re: [tlaplus] About single process system, fairness, and depth-first search option** - Next by thread:
**Re: [tlaplus] TLAPS and primitive-recursive functions** - Index(es):