(New page: ==Overview== -------- For those who are CS geeks like William, the question of whether a function to check whether a system has a given property can be written is very pertinent. I have...) |
|||
| Line 1: | Line 1: | ||
==Overview== | ==Overview== | ||
| − | |||
For those who are CS geeks like William, the question of whether a function to check whether a system has a given property can be written is very pertinent. I have been looking into symbolic math solvers to try to make them do this. | For those who are CS geeks like William, the question of whether a function to check whether a system has a given property can be written is very pertinent. I have been looking into symbolic math solvers to try to make them do this. | ||
| Line 10: | Line 9: | ||
==Basics: Systems as "functions that operate on functions"== | ==Basics: Systems as "functions that operate on functions"== | ||
| − | + | ||
A system can be represented as a function system(x), where x is some function x(t), that returns another function of the form y(t). | A system can be represented as a function system(x), where x is some function x(t), that returns another function of the form y(t). | ||
| Line 16: | Line 15: | ||
In Common LISP, an example of x might be: | In Common LISP, an example of x might be: | ||
:: | :: | ||
| − | + | (setq x (lambda (tt) (+ tt 5))) | |
This corresponds to ``x(t) = t + 5``. ``t`` is a reserved constant in LISP, so I use ``tt``. A ``setq`` here probably isn't the "right way" to do things, but LISP is not my native language. | This corresponds to ``x(t) = t + 5``. ``t`` is a reserved constant in LISP, so I use ``tt``. A ``setq`` here probably isn't the "right way" to do things, but LISP is not my native language. | ||
| Line 22: | Line 21: | ||
At any rate, a simple system to play with would be a time shift. You would represent this as follows (note the extra argument to, representing the amount of time to shift by): | At any rate, a simple system to play with would be a time shift. You would represent this as follows (note the extra argument to, representing the amount of time to shift by): | ||
:: | :: | ||
| − | + | (defun timeshift (x to) (lambda (tt) (funcall x (- tt to)))) | |
You can then represent ``x(t) -> [Shift by to] -> y(t)`` as (in more broken LISP): | You can then represent ``x(t) -> [Shift by to] -> y(t)`` as (in more broken LISP): | ||
:: | :: | ||
| − | + | (setq y (timeshift x 'to)) | |
At this point, you could in theory make a call | At this point, you could in theory make a call | ||
:: | :: | ||
| − | + | (funcall y tt) | |
to get ``y(tt) = x(tt - to) = tt + 5``, but LISP doesn't do symbolic math natively. Thus, some work needs to be done to get AXIOM or some other engine to do the heavy lifting. | to get ``y(tt) = x(tt - to) = tt + 5``, but LISP doesn't do symbolic math natively. Thus, some work needs to be done to get AXIOM or some other engine to do the heavy lifting. | ||
An example using clisp, with commentary: | An example using clisp, with commentary: | ||
:: | :: | ||
| − | + | (setq x (lambda (tt) (+ tt 5))) ; x(tt) = tt + 5 | |
| − | + | (defun timeshift (x to) (lambda (tt) (funcall x (- tt to)))) ; Define the time-shift function | |
| − | + | ; Apply the timeshift to x with to=15. | |
| − | + | ; This is akin to y(t) = x(t - 15) = t - 15 + 5 = t - 10 | |
| − | + | (setq y (timeshift x 15)) | |
| − | + | ; Finally, compute a value of y(t) | |
| − | + | ; y(3) = 3 - 10 = -7 | |
| − | + | (funcall y 3) | |
| Line 51: | Line 50: | ||
==Testing properties== | ==Testing properties== | ||
| − | + | ||
As you can see, using LISP to model systems is potentially a powerful method. The "functions operating on functions" way of thinking can be extended even further to the "system" functions (such as ``timeshift`` above) to prove things about systems. | As you can see, using LISP to model systems is potentially a powerful method. The "functions operating on functions" way of thinking can be extended even further to the "system" functions (such as ``timeshift`` above) to prove things about systems. | ||
Lacking a good symbolic solver, I cannot test the following code yet, but we might write a function "linear" that determines whether the given system function is linear or not. | Lacking a good symbolic solver, I cannot test the following code yet, but we might write a function "linear" that determines whether the given system function is linear or not. | ||
:: | :: | ||
| − | + | (defun islinear (sysfunc) | |
| − | + | (let ((y1 (funcall sysfunc 'x1)) ; Define y1 = sysfunc(x1), y2 = sysfunc(x2) | |
| − | + | (y2 (funcall sysfunc 'x2))) | |
| − | + | (eq | |
| − | + | (+ (* 'a (funcall y1 'tt)) ; a*y1(t) + b*y2(t) = ... | |
| − | + | (* 'b (funcall y2 'tt))) | |
| − | + | (funcall | |
| − | + | (funcall sysfunc | |
| − | + | ; ... = sysfunc(a*x1(t) + b*x2(t))(t) ? | |
| − | + | (lambda (tt) (+ (* 'a (funcall 'x1 tt)) | |
| − | + | (* 'b (funcall 'x2 tt)))) | |
| − | + | ) 'tt) | |
| − | + | ))) | |
Latest revision as of 17:39, 16 March 2008
Overview
For those who are CS geeks like William, the question of whether a function to check whether a system has a given property can be written is very pertinent. I have been looking into symbolic math solvers to try to make them do this.
So far, my most promising lead is the AXIOM solver ( http://wiki.axiom-developer.org/FrontPage ), which might have a LISP interface to its symbolic math engine. This would be ideal.
My notes so far are as follows:
Basics: Systems as "functions that operate on functions"
A system can be represented as a function system(x), where x is some function x(t), that returns another function of the form y(t).
In Common LISP, an example of x might be:
(setq x (lambda (tt) (+ tt 5)))
This corresponds to ``x(t) = t + 5``. ``t`` is a reserved constant in LISP, so I use ``tt``. A ``setq`` here probably isn't the "right way" to do things, but LISP is not my native language.
At any rate, a simple system to play with would be a time shift. You would represent this as follows (note the extra argument to, representing the amount of time to shift by):
(defun timeshift (x to) (lambda (tt) (funcall x (- tt to))))
You can then represent ``x(t) -> [Shift by to] -> y(t)`` as (in more broken LISP):
(setq y (timeshift x 'to))
At this point, you could in theory make a call
(funcall y tt) to get ``y(tt) = x(tt - to) = tt + 5``, but LISP doesn't do symbolic math natively. Thus, some work needs to be done to get AXIOM or some other engine to do the heavy lifting.
An example using clisp, with commentary:
(setq x (lambda (tt) (+ tt 5))) ; x(tt) = tt + 5 (defun timeshift (x to) (lambda (tt) (funcall x (- tt to)))) ; Define the time-shift function
- Apply the timeshift to x with to=15.
- This is akin to y(t) = x(t - 15) = t - 15 + 5 = t - 10
(setq y (timeshift x 15))
- Finally, compute a value of y(t)
- y(3) = 3 - 10 = -7
(funcall y 3)
Again, the lack of native symbolic math operations in LISP is extremely limiting, so a symbolic engine needs to be integrated somehow.
Testing properties
As you can see, using LISP to model systems is potentially a powerful method. The "functions operating on functions" way of thinking can be extended even further to the "system" functions (such as ``timeshift`` above) to prove things about systems.
Lacking a good symbolic solver, I cannot test the following code yet, but we might write a function "linear" that determines whether the given system function is linear or not.
(defun islinear (sysfunc) (let ((y1 (funcall sysfunc 'x1)) ; Define y1 = sysfunc(x1), y2 = sysfunc(x2) (y2 (funcall sysfunc 'x2))) (eq (+ (* 'a (funcall y1 'tt)) ; a*y1(t) + b*y2(t) = ... (* 'b (funcall y2 'tt))) (funcall (funcall sysfunc
- ... = sysfunc(a*x1(t) + b*x2(t))(t) ?
(lambda (tt) (+ (* 'a (funcall 'x1 tt)) (* 'b (funcall 'x2 tt)))) ) 'tt) )))
