Recursively Defined Functions - Revision history

Michael Leuschel: /* Operations applicable for recursive functions */

2016-11-12T13:44:25Z

Operations applicable for recursive functions

← Older revision		Revision as of 13:44, 12 November 2016
Line 100:		Line 100:


	Also, you have to be careful to avoid accidentally expanding these functions. For example, trying to check <tt>parity : INTEGER <-> INTEGER</tt> or <tt>parity : INTEGER +-> INTEGER</tt> will cause ProB to try and expand the function. ~~Future versions of~~ ProB ~~may overcome this limitation~~.		Also, you have to be careful to avoid accidentally expanding these functions. For example, trying to check <tt>parity : INTEGER <-> INTEGER</tt> or <tt>parity : INTEGER +-> INTEGER</tt> will cause older version of ProB to try and expand the function. ProB 1.6.1 can actually check <tt>parity:NATURAL --> INTEGER</tt>, but it cannot check <tt>parity:NATURAL --> 0..1</tt>.

	There are the following further restrictions:		There are the following further restrictions:
	* ProB does not support mutual recursion yet		* ProB does not support mutual recursion yet
	* the function is not allowed to depend on other constants, unless those other constants can be valued in a deterministic way (i.e., ProB finds only one possible solution for them)		* the function is not allowed to depend on other constants, unless those other constants can be valued in a deterministic way (i.e., ProB finds only one possible solution for them)

Michael Leuschel: /* Operations applicable for recursive functions */

2016-11-12T13:42:15Z

Operations applicable for recursive functions

← Older revision		Revision as of 13:42, 12 November 2016
Line 97:		Line 97:
	* apply the function to a given argument, e.g., <tt>parity(100)</tt> will give you 0;		* apply the function to a given argument, e.g., <tt>parity(100)</tt> will give you 0;
	* compute the image of the function, e.g., <tt>parity[1..10]</tt> gives <tt>{0,1}</tt>.		* compute the image of the function, e.g., <tt>parity[1..10]</tt> gives <tt>{0,1}</tt>.
	~~However,~~ composing it with another function (<tt>([1,2] ; parity)</tt>~~) does not work yet. This works for non-recursive infinite functions~~, ~~as described above. Future versions of ProB will probably allow such constructs for recursive functions as well~~.		* composing it with another function, notably finite sequences: <tt>([1,2] ; parity)</tt> corresponds to the "map" construct of functional programming and results in the output <tt>[1,0]</tt>.


	Also, you have to be careful to avoid accidentally expanding these functions. For example, trying to check <tt>parity : INTEGER <-> INTEGER</tt> or <tt>parity : INTEGER +-> INTEGER</tt> will cause ProB to try and expand the function. Future versions of ProB may overcome this limitation.		Also, you have to be careful to avoid accidentally expanding these functions. For example, trying to check <tt>parity : INTEGER <-> INTEGER</tt> or <tt>parity : INTEGER +-> INTEGER</tt> will cause ProB to try and expand the function. Future versions of ProB may overcome this limitation.

Michael Leuschel: /* Recursive Function Definitions in ProB */

2016-11-12T13:37:37Z

Recursive Function Definitions in ProB

← Older revision		Revision as of 13:37, 12 November 2016
Line 83:		Line 83:
	parity : INTEGER <-> INTEGER &		parity : INTEGER <-> INTEGER &
	parity = {0\|->0} \/ %x.(x:NATURAL1\|1-parity(x-1))		parity = {0\|->0} \/ %x.(x:NATURAL1\|1-parity(x-1))
			END

			As of version 1.6.1 you can also use IF-THEN-ELSE and LET constructs in the body of a recursive function. The above example can for example now be written as:
			MACHINE ParityIFTE
			ABSTRACT_CONSTANTS parity
			PROPERTIES
			parity : INTEGER <-> INTEGER &
			parity = %x.(x:NATURAL\|IF x=0 THEN 0 ELSE 1-parity(x-1)END)
	END		END

Michael Leuschel: /* When does ProB treat a set comprehension or lambda abstraction symbolically ? */

2015-10-28T06:46:33Z

When does ProB treat a set comprehension or lambda abstraction symbolically ?

← Older revision		Revision as of 06:46, 28 October 2015
Line 68:		Line 68:
	* <tt>f</tt> is declared to be an <tt>ABSTRACT_CONSTANT</tt> and the equation is part of the <tt>PROPERTIES</tt> with <tt>f</tt> on the left.		* <tt>f</tt> is declared to be an <tt>ABSTRACT_CONSTANT</tt> and the equation is part of the <tt>PROPERTIES</tt> with <tt>f</tt> on the left.
	* the preference <tt>SYMBOLIC</tt> is set to true (e.g., using a <tt>DEFINITION</tt> <tt>SET_PREF_SYMBOLIC == TRUE</tt>)		* the preference <tt>SYMBOLIC</tt> is set to true (e.g., using a <tt>DEFINITION</tt> <tt>SET_PREF_SYMBOLIC == TRUE</tt>)
	* a pragma is used to mark the lambda abstraction as symbolic as follows: <tt>f = /@ symbolic / %x.(PRED\|E)</tt>; this requires ProB version 1.3.5-beta10 or higher.		* a pragma is used to mark the lambda abstraction as symbolic as follows: <tt>f = /@ symbolic / %x.(PRED\|E)</tt>; this requires ProB version 1.3.5-beta10 or higher. In Event-B, pragmas are represented as Rodin database attributes and one should use the [[Tutorial_Symbolic_Constants\|symbolic constants plugin]].

	= Recursive Function Definitions in ProB =		= Recursive Function Definitions in ProB =

Michael Leuschel at 07:41, 27 May 2013

2013-05-27T07:41:49Z

← Older revision		Revision as of 07:41, 27 May 2013
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	[[Category: Advanced Feature]]		[[Category: Advanced Feature]]
			= Symbolic Functions and Relations =
	Take the following function:		Take the following function:
	CONSTANTS parity		CONSTANTS parity

Michael Leuschel: /* When does ProB treat a set comprehension or lambda abstraction symbolically ? */

2013-05-27T07:40:20Z

When does ProB treat a set comprehension or lambda abstraction symbolically ?

← Older revision		Revision as of 07:40, 27 May 2013
Line 67:		Line 67:
	* <tt>f</tt> is declared to be an <tt>ABSTRACT_CONSTANT</tt> and the equation is part of the <tt>PROPERTIES</tt> with <tt>f</tt> on the left.		* <tt>f</tt> is declared to be an <tt>ABSTRACT_CONSTANT</tt> and the equation is part of the <tt>PROPERTIES</tt> with <tt>f</tt> on the left.
	* the preference <tt>SYMBOLIC</tt> is set to true (e.g., using a <tt>DEFINITION</tt> <tt>SET_PREF_SYMBOLIC == TRUE</tt>)		* the preference <tt>SYMBOLIC</tt> is set to true (e.g., using a <tt>DEFINITION</tt> <tt>SET_PREF_SYMBOLIC == TRUE</tt>)
	* a pragma is used to mark the lambda abstraction as symbolic as follows <tt>f = /@ symbolic / %x.(PRED\|E)</tt>; this requires ProB version 1.3.5-beta10 or higher.		* a pragma is used to mark the lambda abstraction as symbolic as follows: <tt>f = /@ symbolic / %x.(PRED\|E)</tt>; this requires ProB version 1.3.5-beta10 or higher.


	= Recursive Function Definitions in ProB =		= Recursive Function Definitions in ProB =

Michael Leuschel at 07:39, 27 May 2013

2013-05-27T07:39:49Z

← Older revision		Revision as of 07:39, 27 May 2013
Line 38:		Line 38:
	** sometimes compute the domain of the function, here, <tt>dom(parity)</tt> is determined to be <tt>NATURAL</tt>. But this only works for simple infinite functions.		** sometimes compute the domain of the function, here, <tt>dom(parity)</tt> is determined to be <tt>NATURAL</tt>. But this only works for simple infinite functions.
	** sometimes check that you have a total function, e.g., <tt>parity: NATURAL --> INTEGER</tt> can be checked by ProB. However, if you change the range (say from <tt>INTEGER</tt> to <tt>0..1</tt>), then ProB will try to expand the function.		** sometimes check that you have a total function, e.g., <tt>parity: NATURAL --> INTEGER</tt> can be checked by ProB. However, if you change the range (say from <tt>INTEGER</tt> to <tt>0..1</tt>), then ProB will try to expand the function.
			** In version 1.3.7 we are adding more and more operators that can be treated symbolically. Thus you can now also compose two symbolic functions using relational composition <tt>;</tt> or take the transitive closure (<tt>closure1</tt>) symbolically.

Michael Leuschel at 07:37, 27 May 2013

2013-05-27T07:37:09Z

← Older revision		Revision as of 07:37, 27 May 2013
Line 61:		Line 61:
	You may also want to look at the tutorial page on [[Tutorial_Modeling_Infinite_Datatypes\|modeling infinite datatypes]].		You may also want to look at the tutorial page on [[Tutorial_Modeling_Infinite_Datatypes\|modeling infinite datatypes]].

			== When does ProB treat a set comprehension or lambda abstraction symbolically ? ==
	Currently there are four cases when ProB tries to keep a function such as <tt>f = %x.(PRED\|E)</tt> symbolically rather than computing an explicit representation:		Currently there are four cases when ProB tries to keep a function such as <tt>f = %x.(PRED\|E)</tt> symbolically rather than computing an explicit representation:
	* the domain of the function is obviously infinite; this is the case for predicates such as <tt>x:NATURAL</tt>; in version 1.3.7-beta5 or later this has been considerably improved. Now ProB also keeps those lambda abstractions or set comprehensions symbolic where the constraint solver cannot reduce the domain of the parameters to a finite domain. As such, e.g., <tt>{x,y,z\| xx + yy = z*z}</tt> or <tt>{x,y,z\| z:seq(NATURAL) & x^y=z}</tt> are now automatically kept symbolic.		* the domain of the function is obviously infinite; this is the case for predicates such as <tt>x:NATURAL</tt>; in version 1.3.7-beta5 or later this has been considerably improved. Now ProB also keeps those lambda abstractions or set comprehensions symbolic where the constraint solver cannot reduce the domain of the parameters to a finite domain. As such, e.g., <tt>{x,y,z\| xx + yy = z*z}</tt> or <tt>{x,y,z\| z:seq(NATURAL) & x^y=z}</tt> are now automatically kept symbolic.
Line 83:		Line 84:
	END		END

			== Operations applicable for recursive functions ==
	With such a recursive function you can:		With such a recursive function you can:
	* apply the function to a given argument, e.g., <tt>parity(100)</tt> will give you 0;		* apply the function to a given argument, e.g., <tt>parity(100)</tt> will give you 0;

Michael Leuschel at 07:35, 27 May 2013

2013-05-27T07:35:45Z

← Older revision		Revision as of 07:35, 27 May 2013
Line 62:		Line 62:

	Currently there are four cases when ProB tries to keep a function such as <tt>f = %x.(PRED\|E)</tt> symbolically rather than computing an explicit representation:		Currently there are four cases when ProB tries to keep a function such as <tt>f = %x.(PRED\|E)</tt> symbolically rather than computing an explicit representation:
	* the domain of the function is obviously infinite; this is the case for predicates such as <tt>x:NATURAL</tt>		* the domain of the function is obviously infinite; this is the case for predicates such as <tt>x:NATURAL</tt>; in version 1.3.7-beta5 or later this has been considerably improved. Now ProB also keeps those lambda abstractions or set comprehensions symbolic where the constraint solver cannot reduce the domain of the parameters to a finite domain. As such, e.g., <tt>{x,y,z\| xx + yy = z*z}</tt> or <tt>{x,y,z\| z:seq(NATURAL) & x^y=z}</tt> are now automatically kept symbolic.
	* <tt>f</tt> is declared to be an <tt>ABSTRACT_CONSTANT</tt> and the equation is part of the <tt>PROPERTIES</tt> with <tt>f</tt> on the left.		* <tt>f</tt> is declared to be an <tt>ABSTRACT_CONSTANT</tt> and the equation is part of the <tt>PROPERTIES</tt> with <tt>f</tt> on the left.
	* the preference <tt>SYMBOLIC</tt> is set to true (e.g., using a <tt>DEFINITION</tt> <tt>SET_PREF_SYMBOLIC == TRUE</tt>)		* the preference <tt>SYMBOLIC</tt> is set to true (e.g., using a <tt>DEFINITION</tt> <tt>SET_PREF_SYMBOLIC == TRUE</tt>)
	* a pragma is used to mark the lambda abstraction as symbolic as follows <tt>f = /@ symbolic / %x.(PRED\|E)</tt>; this requires ProB version 1.3.5-beta10 or higher.		* a pragma is used to mark the lambda abstraction as symbolic as follows <tt>f = /@ symbolic / %x.(PRED\|E)</tt>; this requires ProB version 1.3.5-beta10 or higher.


	= Recursive Function Definitions in ProB =		= Recursive Function Definitions in ProB =

Michael Leuschel at 12:51, 18 March 2013

2013-03-18T12:51:38Z

← Older revision		Revision as of 12:51, 18 March 2013
Line 31:		Line 31:
	** apply the function, e.g., <tt>parity(10001)</tt> is the value <tt>1</tt>		** apply the function, e.g., <tt>parity(10001)</tt> is the value <tt>1</tt>
	** compute the image of the function, e.g., <tt>parity[10..20]</tt> is <tt>{0,1}</tt>		** compute the image of the function, e.g., <tt>parity[10..20]</tt> is <tt>{0,1}</tt>
			** check if a tuple is a member of the function, e.g., <tt>20\|->0 : parity</tt>
			** check if a tuple is not a member of the function, e.g., <tt>21\|->0 /: parity</tt>
			** check if a finite set of tuples is a subset of the function, e.g., <tt>{20\|->0, 120\|->0, 121\|->1, 1001\|->1} <: parity</tt>
			** check if a finite set of tuples is not a subset of the function, e.g., <tt>{20\|->0, 120\|->0, 121\|->1, 1001\|->2} /<: parity</tt>
	** compose the function with a finite relation, e.g., <tt>(id(1..10) ; parity)</tt> gives the value <tt>[1,0,1,0,1,0,1,0,1,0]</tt>		** compose the function with a finite relation, e.g., <tt>(id(1..10) ; parity)</tt> gives the value <tt>[1,0,1,0,1,0,1,0,1,0]</tt>
	** sometimes compute the domain of the function, here, <tt>dom(parity)</tt> is determined to be <tt>NATURAL</tt>. But this only works for simple infinite functions.		** sometimes compute the domain of the function, here, <tt>dom(parity)</tt> is determined to be <tt>NATURAL</tt>. But this only works for simple infinite functions.