Tla+ through examples (XI) -- propositional logic and examples

Propositional logic and examples

Logic symbols have been used in previous examples , Mainly \A ,\E, => Equisign .

\E

E yes "exists" The first letter of , It means existence . When writing down \E x \in S : P(x) It means in S There is at least one x bring P It's true . use \E The return value of the first expression is Boolean .

\E x \in {1,2} : x > 0   by  true
\E x \in {} : x > 0   by  false

\E It means that there is an element that meets the condition ,~\E There is no element that meets the condition

\A

A Of "All" The first letter of , When writing down \A x \in S : P(x) Means for S All elements in ,P It's all true . When there is an element that makes P When it is false , Then the expression returns FALSE.

\A x \in {} : FALSE  = TRUE  

~\A And \A It means the opposite .

=> and <=>

P => Q intend If P It's true , that Q It's true . Be careful ：P When it is false ,Q It can also be true . stay TLC in P => Q Equivalent to ~P / Q.

P <=> Q intend P and Q Both are true or false . amount to (~P /\ ~Q) / (P /\ Q)

 Be careful ：=>  And  <=>  As a logical connector , And /\ and \/ Have the same priority , The indentation rule is the same .

example

1、 Given a set of numbers S And a number N, Define an expression , Return whether it can be in S Find N Elements make this N The sum of these elements is 0.

\*  The topic can be broken down into ：1、 from S Found a subset in ,2  The length of the subset is N,3, Find the sum of the elements of the subset  4、 There is a subset , The sum of elements is equal to 0
\*  Find a subset with length N A set of sets of 
Op2(S,n) == { e \in SUBSET S : Cardinality(e) = n }
\*  Find the sum of set elements 
RECURSIVE Sum(_)
Sum(S) == IF S = {} THEN 0
          ELSE LET x == CHOOSE x \in S : TRUE
                         IN  x + Sum(S \ {x})
\*  Define expressions 
Sum2Zero(S,N) == \E e \in Op2(S,N) : Sum(e)=0

2、 Given an expression Op(,_) And a collection S, Define an expression , Return expression for set S Whether all elements in are exchangeable . for example IsCommutative(Add(_,_),{1,2}) = TRUE , because Add(1,2) and Add(2,1) equal .

IsCommutative(Op(_,_), S) == \A x \in S, y \in S : Op(x,y) = Op(y,x)

3、 Given a set , Returns the maximum number in the set

Max(S) == CHOOSE x \in S : \A y \in S : y <= x 
\*  Note that the judgment here must be <= , It can't be <. Because there is no number bigger than itself .

4、 Given a set S, If the elements in the set p Prime number ,p-2 It's a prime number or p+2 Prime number , be p Twins are prime numbers . seek S The largest twin prime number in .

\* 1、 Find out whether a number is a prime number 
IsPrime(x) == x > 1 /\ ~\E d \in 2..(x-1) : x % d = 0
\* 2、 Find out whether a number is a twin prime number 
IsTwinPrime(a) == /\ IsPrime(a) /\ (IsPrime(a-2) \/ IsPrime(a+2))
\* 3、 Find the set of twin primes 
GetTwinPrime(S) == { a \in S : IsTwinPrime(a)}
\* 4、 Find the maximum twin prime 
LargestTwinPrime(S) == CHOOSE x \in GetTwinPrime(S): \A y \in GetTwinPrime(S) : x >=y 

5、 Returns the largest pair of twin primes in the above set , If a twin prime is missing , Then the pair is invalid . for example ：{3,5,13} The largest twin prime pair of is <<3,5>>, because 13 The twin prime of 11 Not in the assembly .

\* 1、 Find the set of twin prime pairs from the set of twin prime numbers , If a,a+2 All in the set , The retention a.
GetPairTwinPrime(S) == { a \in GetTwinPrime(S): a+2 \in GetTwinPrime(S)}
\* 2、 Find the maximum value from the set of twin prime pairs x, that <<x,x+2>> That's what I'm looking for 
LargestPariTwinPrime(S) == LET x == CHOOSE x \in GetPairTwinPrime(S) : 
						     \A y \in GetPairTwinPrime(S) : x >=y
                           	IN <<x,x+2>>

6、 Given a positive integer tuple stockprices Used to express the change of stock value during the day , Write an operator to determine the maximum profit you can make , Suppose you can only buy and sell first and buy and sell at most once .

\*  Can only buy and sell 1 Time , Just find the largest difference between the two numbers ,
\*  Only buy first and then , You need to subtract the previous number from the latter number 
\* 1、 Convert tuples into tuple pairs , And the first element is in front of the second element 
\*  for example <<1,2,3>>  Turn into  <<1,2>>,<<1,3>>,<<2,3>> Equivalent to {1} \X {2,3} \union {2} \X {3} 
RECURSIVE newSxS(_)
newSxS(S) == IF Len(S) > 1 
                THEN LET newset== <<{Head(S)},{S[t]:t \in 2..Len(S)}>>
                       IN newset[1] \X newset[2] \union  newSxS(Tail(S))
                      
             ELSE {}
\*  Choose from the binary set <<x,y>> The one with the largest difference is ok              
MaxProfit(stockprices) == LET sxs == newSxS(stockprices)
                             IN LET res == CHOOSE <<x,y>> \in sxs: 
                                         \A <<a,b>> \in sxs : y-x >= b-a 
                                IN IF res[2]-res[1] > 0 THEN res[2]-res[1]
                                   ELSE 0  \*  If there is no profit, do not operate . If you have to buy and sell once , Then return to res[2]-res[1] that will do