Mathematica 4.0 for Solaris
Copyright 1988-1999 Wolfram Research, Inc.
 -- Terminal graphics initialized -- 
Loading MMAlpha...
Unix version 
Alpha v1.0 Initialization
The Documentation can be found in /udd/alpha/alpha_beta/Mathematica/doc/user
Current version in /udd/alpha/alpha_beta/Mathematica
Current directory=/udd/alpha/alpha_beta/Mathematica/demos/NOTEBOOKS/Introducti
  on
 
If you use the notebook interface,  you can open the master notebook by
 typing: start[].

In[1]:= setMMADir[{"demos", "NOTEBOOKS", "Introduction"}]


Out[1]= /udd/alpha/alpha_beta/Mathematica/demos/NOTEBOOKS/Introduction

In[2]:= In[2]:= load["exemple2.alpha"]; ashow[]
[exemple2]
 Library Loaded
system exemple2 (x : {t | 1>=0} of integer; 
                 y : {t | 1>=0} of integer)
       returns  (z : {t | 2<=t} of integer);
var
  S : {t | 2<=t} of integer;
let
  S[t] = (x + y)[t-1];
  z[t] = S[t];
tel;

In[3]:= normalize[]; ashow[]
system exemple2 (x : {t | 1>=0} of integer; 
                 y : {t | 1>=0} of integer)
       returns  (z : {t | 2<=t} of integer);
var
  S : {t | 2<=t} of integer;
let
  S[t] = x[t-1] + y[t-1];
  z[t] = S[t];
tel;

In[4]:= save[$tmpDirectory<>"exemple2.alpha"];

In[5]:= load["exemple3wrg.alpha"]; ashow[]
[exemple3]
 Library Loaded
system exemple3 (x : {t | 1<=t} of integer; 
                 y : {t | 1<=t} of integer)
       returns  (z : {t | 2<=t} of integer);
var
  S : {t | 1<=t} of integer;
let
  S[t] = x[t-1] + y[t-1];
  z[t] = S[t];
tel;

In[6]:= analyze[]
 
Static Analysis of system exemple3
--Checking declaration of variables.
--Checking single assignment rule.
--Checking definitions of output/local variables.
--Checking definition of input variables.
--Checking that input/local variables are used.
--Checking type and domain consistency in the equations:
----equation defining S
ERROR: Variable S not defined over the domain :
{t | t=1}
 
----equation defining z

*** Analysis failed ***

Out[6]= False

In[7]:= load["exemple2.alpha"]; ashow[]
[exemple2]
 Library Loaded
system exemple2 (x : {t | 1>=0} of integer; 
                 y : {t | 1>=0} of integer)
       returns  (z : {t | 2<=t} of integer);
var
  S : {t | 2<=t} of integer;
let
  S[t] = (x + y)[t-1];
  z[t] = S[t];
tel;

In[8]:= substituteInDef["z", "S"]; show[]
system exemple2 (x : {t | 1>=0} of integer; 
                 y : {t | 1>=0} of integer)
       returns  (z : {t | 2<=t} of integer);
var
  S : {t | 2<=t} of integer;
let
  S = (x + y).(t->t-1);
  z = ({t | 2<=t} : (x + y).(t->t-1)).(t->t);
tel;

In[9]:= normalize[]; ashow[]
system exemple2 (x : {t | 1>=0} of integer; 
                 y : {t | 1>=0} of integer)
       returns  (z : {t | 2<=t} of integer);
var
  S : {t | 2<=t} of integer;
let
  S[t] = x[t-1] + y[t-1];
  z[t] = x[t-1] + y[t-1];
tel;

In[10]:= unusedVarQ["S"]

Out[10]= True

In[11]:= removeAllUnusedVars[]; ashow[]
system exemple2 (x : {t | 1>=0} of integer; 
                 y : {t | 1>=0} of integer)
       returns  (z : {t | 2<=t} of integer);
let
  z[t] = x[t-1] + y[t-1];
tel;

In[12]:= load["exemple9.alpha"]; ashow[]
[exemple9]
 Library Loaded
system exemple9 (x : {t,p | 1<=t; 1<=p<=4} of integer; 
                 y : {t,p | 1<=t; 1<=p<=4} of integer)
       returns  (z : {t | 1<=t} of integer);
var
  Z : {t,p | 1<=t; 0<=p<=4} of integer;
  S : {t,p | 1<=t; 1<=p<=4} of integer;
let
  S[t,p] = x[t,p] + y[t,p];
  Z[t,p] = 
      case
        { | p=0} : 0[];
        { | 1<=p} : Z[t,p-1] + S[t,p];
      esac;
  z[t] = Z[t,4];
tel;

In[13]:= changeOfBasis["Z.(t,p->t+p,p)"]; ashow[]
system exemple9 (x : {t,p | 1<=t; 1<=p<=4} of integer; 
                 y : {t,p | 1<=t; 1<=p<=4} of integer)
       returns  (z : {t | 1<=t} of integer);
var
  Z : {t,p | p+1<=t; 0<=p<=4} of integer;
  S : {t,p | 1<=t; 1<=p<=4} of integer;
let
  S[t,p] = x[t,p] + y[t,p];
  Z[t,p] = 
      case
        { | p=0} : 0[];
        { | 1<=p} : Z[t-1,p-1] + S[t-p,p];
      esac;
  z[t] = Z[t+4,4];
tel;

In[14]:= substituteInDef["Z", "Z"]; ashow[]
system exemple9 (x : {t,p | 1<=t; 1<=p<=4} of integer; 
                 y : {t,p | 1<=t; 1<=p<=4} of integer)
       returns  (z : {t | 1<=t} of integer);
var
  Z : {t,p | p+1<=t; 0<=p<=4} of integer;
  S : {t,p | 1<=t; 1<=p<=4} of integer;
let
  S[t,p] = x[t,p] + y[t,p];
  Z[t,p] = 
      case
        { | p=0} : 0[];
        { | 1<=p} : ({t,p | p+1<=t; 0<=p<=4} : 
              case
                {t,p | p=0} : 0.(t,p->);
                {t,p | 1<=p} : Z.(t,p->t-1,p-1) + S.(t,p->t-p,p);
              esac)[t-1,p-1] + S[t-p,p];
      esac;
  z[t] = Z[t+4,4];
tel;

In[15]:= normalize[]; ashow[]
system exemple9 (x : {t,p | 1<=t; 1<=p<=4} of integer; 
                 y : {t,p | 1<=t; 1<=p<=4} of integer)
       returns  (z : {t | 1<=t} of integer);
var
  Z : {t,p | p+1<=t; 0<=p<=4} of integer;
  S : {t,p | 1<=t; 1<=p<=4} of integer;
let
  S[t,p] = x[t,p] + y[t,p];
  Z[t,p] = 
      case
        { | p=0} : 0[];
        { | 2<=t; p=1} : 0[] + S[t-p,p];
        { | p+1<=t; 2<=p<=5} : Z[t-2,p-2] + S[t-p,p-1] + S[t-p,p];
      esac;
  z[t] = Z[t+4,4];
tel;

In[16]:= simplifySystem[]; ashow[]
system exemple9 (x : {t,p | 1<=t; 1<=p<=4} of integer; 
                 y : {t,p | 1<=t; 1<=p<=4} of integer)
       returns  (z : {t | 1<=t} of integer);
var
  Z : {t,p | p+1<=t; 0<=p<=4} of integer;
  S : {t,p | 1<=t; 1<=p<=4} of integer;
let
  S[t,p] = x[t,p] + y[t,p];
  Z[t,p] = 
      case
        { | p=0} : 0[];
        { | p=1} : 0[] + S[t-1,p];
        { | 2<=p} : Z[t-2,p-2] + S[t-p,p-1] + S[t-p,p];
      esac;
  z[t] = Z[t+4,4];
tel;

In[17]:=