File: RequiredValues.md

package info (click to toggle)
curry-tools 1.0.1%2Bdfsg1-1
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 5,492 kB
  • ctags: 121
  • sloc: makefile: 470; sh: 421
file content (32 lines) | stat: -rw-r--r-- 1,135 bytes parent folder | download | duplicates (7)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
Required values analysis
------------------------

This analysis checks for each operation in a Curry program whether
the arguments must have a particular shape in order to
compute some value.
For instance, the negation operation `not` defined by

    not True  = False
    not False = True

requires the argument value `False` in order to compute the result
`True` and it requires the argument `True` to compute the result
`False`. This property is expressed by the following abstract type:

    not : ({True} -> {False}) | ({False} -> {True})

Hence, each abstract type is a set of constructors which represents
all expressions rooted by one of the constructors in this set.
Moreover, the abstract type `any` denotes any expression.
The empty list denotes an impossible required type, i.e.,
an argument which is required but for which no applicable value exists.
For instance, the operation

    f x = solve (x && not x)

has the required value typing

    f: ({} -> True)

A detailed description of this analysis and its application can be found in the
[LOPSTR'15 paper](http://www.informatik.uni-kiel.de/~mh/papers/LOPSTR15.html).