Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
research:software:gradual-unions [2017/05/02 09:42] – [Installation instructions] mtoro | research:software:gradual-unions [2017/05/02 10:30] – [A first example] mtoro | ||
---|---|---|---|
Line 35: | Line 35: | ||
We also provide the steps required to start the web server manually in case it does not start automatically: | We also provide the steps required to start the web server manually in case it does not start automatically: | ||
- | - For sudo privileges the username is gradualunions and the password is 1234 | + | - For sudo privileges the username is "gradualunions" |
- | - Open a terminal. (Make sure you are at home.) | + | - Open a terminal |
- Run <code bash> | - Run <code bash> | ||
service gradual-unions start | service gradual-unions start | ||
</ | </ | ||
- | - We provide the restart and stop commands as well. | + | |
+ | | ||
To change the port of the application, | To change the port of the application, | ||
Line 48: | Line 49: | ||
/ | / | ||
</ | </ | ||
- | To run the application not as a service | + | To run the application not as a service, look at the next section (steps 4 and 5). |
Line 72: | Line 73: | ||
</ | </ | ||
- | To kill the application, | + | To kill the application, |
Note that to run again the implentation, | Note that to run again the implentation, | ||
Line 101: | Line 102: | ||
A term can be a typed lambda abstraction, | A term can be a typed lambda abstraction, | ||
- | Types can be booleans Bool, integers Int, unknown | + | Types can be booleans |
==== The action area ==== | ==== The action area ==== | ||
Line 131: | Line 132: | ||
{{: | {{: | ||
- | Each step shows in red the redux. | + | Each step shows the redux in red. |
- | Note as program may loop infinitely (we can encode omega), the prototype only present the first 10 steps of reduction. If after 10 steps of reduction the program is still reducible, another button is presented to reduce another 10 steps. | + | Note as program may loop infinitely (with ''?'' |
The reduction of the program is presented as the reduction of intrinsic terms: derivation trees augmented with evidence. An evidence reflects the justification of why a given consistent judgment holds. | The reduction of the program is presented as the reduction of intrinsic terms: derivation trees augmented with evidence. An evidence reflects the justification of why a given consistent judgment holds. | ||
Line 174: | Line 175: | ||
This is an example of combining the use of gradual unions and the unknown type. The applied lambda receives either a function that receives an Int, or a function that returns an Int. | This is an example of combining the use of gradual unions and the unknown type. The applied lambda receives either a function that receives an Int, or a function that returns an Int. | ||
- | {{: | + | {{: |
This program, as we are passing a function from Int to Int the program run without errors. | This program, as we are passing a function from Int to Int the program run without errors. | ||
Now consider the following program: | Now consider the following program: | ||
- | {{: | + | {{: |
This time we are passing as argument a function from Bool to Int, so the program also run without errors. | This time we are passing as argument a function from Bool to Int, so the program also run without errors. |