Tautology and Contradiction

 We will see here how we can construct truth tables for finding tautology and contradiction. We use here static functions (Called with @ before name) and subs, which are part of same "parent" module, where parent means here a module/function which contains source of child functions/modules. Static functions and sub aren't owner of a scope, but any local variable removed at the exit/return from the call. One reason for anyone to use a static part of code, is the compactness of code.

Modules and normal functions have own scope, and we can call anything we define there, but not something which an inner module define. To use something defined before the call of a module we have to pass it as parameter, or to have it as global. Any local definition hide any global with same name, but if we call an inner module the global one aren't hidden until we define a same name definition.

Identifier True and False are double type values -1 and 0, so here we want to be Boolean. One way to do that is by defining constants. The values after boolean= can be zero or non zero, or False and True (which are the standard True and False, not the new defined).

Especially for global constants we can use a statement like const True, False to check if these constants exist as user's constants (not the predefined True and False). If we place a const bool True =@True which make a local constant then we hide the global one, and this isn't bad, because we have the same result here, but if we need to use a constant value say 1234 which defined globally (until the module which define it exit execution), with a name ABC, a statement ABC=100 make a local variable which hide the global constant, and change the ABC from constant to a variable. So if we use Const ABC without providing a value, interpreter check if there is a global constant ABC and if found one make a reference ABC as local to the global constant, so now a ABC=100 will raise error, because ABC exist as  local constant. If nothing found, at Const ABC statement, interpreter raise error, for missing constant.

In M2000 not all inner modules defined on same source as the parent. We can load modules from disk using Load statement on any module or function.  Interpreter use a cashed list of functions depending on loading modules, and we can exclude cash list using properly the load function.

Module CanonicalForms2 {
	Font "Verdana"
	linespace 0
	form 60
	global const True as boolean=True, False as boolean=False
	module tautology {
		const True, False
		print part "  tautology based on truth table: P ∨ ¬P"
		print Under $(7),"P", "¬P", "P ∨ ¬P"
		print under
		P = (True, False)
		Q = (True, False)
		eP = Each(P)
		boolean acc=true
		While eP
			acc = acc and @P() or not @P()
			print @P(), not @P(), @P() or not @P() 
		end While
		tautology(acc)
		print
		print part "  tautology based on truth table: P → (Q → P)"
		print Under $(7),"Q", "P", "Q → P", "P → (Q → P)"
		print Under
		acc = True
		eP = Each(P)
		While eP
			eQ=Each(Q)
			While eQ
				acc = acc and @implication(@P(), @implication(@Q(),@P()))
				print @Q(), @P(),  @implication(@Q(),@P()), @implication(@P(), @implication(@Q(),@P()))
			end While
		end While	
		tautology(acc)
		print	
	}
	module contradiction {
		const True, False
		print part "  contradiction based on truth table: P ∧ ¬P"
		print Under $(7),"P", "¬P", "P ∧ ¬P"
		print under
		P = (True, False)
		Q = (True, False)
		eP = Each(P)
		boolean acc=false
		While eP
			acc = acc or @P() and not @P()
			print @P(), not @P(), @P() and not @P() 
		end While
		contradiction(acc)
		print
		print
		print part " contradiction based on truth table: ¬(P ∨ ¬(P ∧ Q))"
		print Under $(7),"P", "Q", "P ∧ Q","¬(P ∧ Q)", "P ∨ ¬(P ∧ Q)","¬(P ∨ ¬(P ∧ Q))"
		print Under
		acc = false
		eP = Each(P)
		While eP
			eQ=Each(Q)
			While eQ
				acc = acc and not (@P() or not (@P() and @Q()))
				print @P(), @Q(), @P() and @Q(), not (@P() and @Q()),
				print @P() or not (@P() and @Q()), not (@P() or not (@P() and @Q()))
			end While
		end While	
		contradiction(acc)
	}
	module check_for_contradiction_or_tautology {
		const True, False
		print
		print part "  check for contradiction and tautology: (P → Q)→ P"
		print Under $(7),"P", "Q", "P → Q", "(P → Q)→ P"
		print under
		P = (True, False)
		Q = (True, False)
		eP = Each(P)
		boolean acc1=true, acc2=false, res
		While eP
			eQ=Each(Q)
			While eQ
				res = @implication(@implication(@P(),@Q()),@P())
				acc1 = acc1 and res
				acc2 = acc2 or res
				print @P(), @Q(), @implication(@P(),@Q()), res
			end While
		end While
		tautology(acc1)
		contradiction(acc2)
	}
	tautology
	contradiction
	check_for_contradiction_or_tautology
	push key$
	drop
	// inner modules can found static functions on the parent, which are in the same code
	// but variables scope isn't extend to parent.
	// So eP and eQ must defined prior to call  these functions
	function implication(P as boolean, Q as boolean)
		// canonical form
		=Not P Or Q
	end function
	function P()
		=array(eP)
	end function
	function Q()
		=array(eQ)
	end function
	sub tautology(acc as boolean)
		if acc then
			print  "we have tautology, all True"
		else
			print  "we haven't tautology, not all True"
		end if
	end sub
	sub contradiction(acc as boolean)
		if not acc then
			print  "we have contradiction, all False"
		else
			print  "we haven't contradiction, not all False"
		end if
	end sub
}
CanonicalForms2

Canonical Forms for Logical implication and equivalence (new)

We see here how and why we use two types of functions, plus the object of the example to print truth tables for some functions.

Here we make a program for displaying  truth tables for two functions the implication and equivalence. Because True and False are of type Double (-1 and 0), we make them as Boolean types, so at the Print statement we get True and False (right justified as numbers). All comparisons and logical expressions return  result as Boolean type. A non zero number converted to True so 15 and 3 return True, but binary.and(15, 3) return 3.

We use two types of functions, normal functions like implication() and equivalence() and simple functions P() and Q() which have to call as @P() and @Q(). Simple functions use module scope, so eP and eQ can be used. Normal functions have own scope. The True as Boolean can be used inside implication (but here we didn't use it), because we declare it as Global (for the lifetime of module CanonicalForm1, and from the line we defined it). Modules and Functions which called them with normal call can't be see anything out of them, and anything inside other modules/functions which we define in these modules/functions. Normal functions can call themselves. Simple functions can call anything defined in module as far, and always simple functions. When we first time call a simple function a search begin from the end to start until interpreter found it, and then register to a fast call list, for the next time we call it again. Normal functions works different. The function's code loaded in a list with a key to the specific defined identifier, using a hash table. So we can reload another function code if we wish. Also normal functions can be passed by reference, but simple functions can't. A lambda function is a normal function with a list of closures, where these closures are every time in scope with code of lambda and any recursive call (we use Lambda() to call the current function). Simple functions can use recursion, using the defined name of current simple function.

Other difference between simple functions and other (normal/lambda): 

• A simple function can't be called like a module using Call statement, but only in expressions. 
• We have to use Local to define variables and arrays for local use on simple functions. All other have own scope, so anything defined by default is local.
• Stack of values (used also for passing parameters) are the same as the module's stack of values for simple functions so we can't easy use variadic call for functions. Normal and Lambda functions when we call them in expressions we pass a new stack of values with any parameter value on it, and only for the specific call (the stack erased at the exit). At recursion simple functions still use the same stack of values, but normal and lambda function use a new one for every call.
• We can't pass by reference an array item or a static variable to a simple function. We can do this for normal and lambda functions.

An example about passing array item and static variable to a normal function:

Module TestByRef {
	Dim a(10)=3
	Static Z=100
	Function k(&m) {
		=m
		m++
	}
	Print a(3)
	Print k(&a(3))
	Print a(3)
	Print Z
	Print k(&Z)
	Print Z
}
TestByRef
TestByRef
Clear  // clear variables, no functions/modules
TestByRef

And this is an example using simple function (the m in function k() is local by default):

Module TestByRef1 {
	m=10
	Print m
	Print @k(&m)
	Print m
	Function k(&m)
		=m
		m++
	End Function

}
TestByRef1

The final example. This program use Unicode symbols from here

Module CanonicalForms1 {
	Font "Verdana"
	Mode 15.5  // 15.5 pt size current font
	// make True and False as boolean values
	Global Boolean True=@True, False=@False
	Function implication(P as boolean, Q as boolean) {
		// canonical form
		=Not P Or Q
	}
	Function equivalence(P as boolean, Q as boolean) {
		//canonical form
		=(Not P Or Q) And (Not Q Or P)
	}
	Print part "  implication truth table: (P → Q) ⇒ ¬P ∨ Q"
	Print Under $(7),"P", "Q", "(P → Q)"
	Print under
	P=(True, False)
	Q=(True, False)
	eP=Each(P)
	While eP
		eQ=Each(Q)
		While eQ
			Print @P(), @Q(), implication(@P(),@Q())
		End While
	End While
	Print
	Print part "  equivalence truth table: (P ↔ Q) ⇔ (P → Q) ∧ (Q → P)"
	Print Under $(7),"P", "Q", "(P ↔ Q)"
	Print under
	eP=Each(P)
	While eP
		eQ=Each(Q)
		While eQ
			Print @P(), @Q(), equivalence(@P(),@Q())
		End While
	End While
	
	Print
	Print part "  logical AND truth table: P ∧ Q"
	Print Under $(7),"P", "Q", "(P ∧ Q)"
	Print under	
	eP=Each(P)
	While eP
		eQ=Each(Q)
		While eQ
			Print @P(), @Q(), @P() and @Q()
		End While
	End While	
	
	Print
	Print part "  logical OR truth table: P ∨ Q"
	Print Under $(7),"P", "Q", "(P ∨ Q)"
	Print under	
	eP=Each(P)
	While eP
		eQ=Each(Q)
		While eQ
			Print @P(), @Q(), @P() or @Q()
		End While
	End While	
	
	Print
	Print part "  logical NOT truth table: ¬P"
	Print Under $(7),"P","", "(¬P)"
	Print under	
	eP=Each(P)
	While eP
		Print @P(), "", not @P()
	End While
		
	Function P()
		=array(eP)
	End Function
	Function Q()
		=array(eQ)
	End Function
}
CanonicalForms1

Find set of Differences from two sets of type item

 This is a simple program, which use a type item as enum type, and lists as automatic arrays (tuple). Also we use the current stack of values and the formula array([]) which leave an empty stack of values, and return an array of item converting the stack object to array object. The [] identifier return the stack of values, while leave an empty stack (So we didn't get a pointer to current stack of values, that not allowed from interpreter). The array() functions if get a stack pointer make a new tuple and move all elements from stack object to array object

Look this sample code. Variable k is of type mStiva, use Type$(k) to get the name. Length of k is 3, the we make L as array(k) so length of L is 3 but length of k is 0. To preserve items on k we have to use L=array(stack(k)). Function stack() return a new stack object.

k=stack:=1,2,3
Print Len(k)=3
L=array(k)
Print Len(k)=0
Print Len(L)=3

We can produce a stack item from an array (a tuple), but without reducing items on that array. Always we get shallow copies, so if we have pointers to arrays, these are just copies of these pointers not the arrays as is.

m=stack(L)
Print type$(m)="mStiva"
Print Len(L)=3
Print Len(M)=3

The program:

Module TestDiff {
	// Find differnences of two set of items of type item
	Enum item {
		pig=random(-20, 1000), cat, dog, cow, elephant, mice, horse
	}
	
	ListA=(pig, cow, elephant, mice)
	ListB=(dog, cat, pig, mice)
	
	k=min.data(len(ListA), len(ListB))
	if len(ListB)=k then M1=ListA : M2=ListB else M2=ListA:M1=ListB
	M=each(M1)
	flush
	integer nullitem=pig-1
	dim a(pig to horse)=nullitem
	
	While M
		i=array(M)
		a(i)=i
	End While	
	M=each(M2)
	While M
		i=array(M)
		if a(i)=i then a(i)=nullitem else a(i)=i
	End While
	M=each(a())
	flush
	While M
			if array(m)>0 then push array(M)
	End While
	Pen 15 {
		dispnames(ListA, "ListA")
		dispnames(ListB, "ListB")
	}
	
	if empty then
		print "no differences found"
	else
		M3=Array([])
		Pen 11 {
			dispnames(M3,"Differences")
		}
	End if
	Sub dispnames(k as array, title$)
		Local M=each(k)
		Stack new {
			While M
				Data eval$(array(M))
			End While
			print title$;": ";array([])#str$(", ")
		}
	End Sub
}
TestDiff