1.4. Built-in data types

DynSem has built-in support for the following types:

1.4.1. Numbers

Premises on numbers
a == b
Equality check. Fails if the two numbers are not equal. a and b may be bound variables or number literals.
a != b
Inequality check. Fails if the two numbers are equal. a and b may be bound variables or number literals.
a => b
Equivalent to == if b is a number literal. Binds new variable b to the value of a if b is an unbound variable. Invalid if b is a bound variable.
a =!=> b
Equivalent to != if b is a number literal. Invalid if b is a variable (bound or unbound).
case a of { b => ... }
Switch-like premise for multiple cases. a must either be a number literal or a bound variable. b must either be a number literal or an unbound variable.

One can write reduction rules directly on numbers, for example:

module nums

signature
  arrows
    Int -inc-> Int

rules
  3 -inc-> 4

Int

The sort Int denotes positive and negative whole numbers, e.g. 3, 99, -49. The range of is the same as Java’s int range: -2,147,483,648 to 2,147,483,647.

Integers can be typed literally, read or written from variables and matched against. Int terms are coerceable to Float where needed.

Long

Similar to Int, except for the range being the same as Java’s long range: -9,223,372,036,854,775,808 to 9,223,372,036,854,775,807.

Long values are coercible to Real where needed.

Float

The sort Float denotes positive and negative decimal numbers, e.g. 3.14, 9.99, -42.42. The range is the same as Java’s float range. Float inherits the precision of Java’s float.

All Int operations are supported on Float. Note that due to precision issues equality/match checks between decimal vaues may unexpectedly fail.

Float values are coercible to Real where needed.

Real

The sort Real denotes large positive and negative decimal numbers. The range is the same as Java’s double.

All Int operations are supported on Real. Note that due to precision issues equality/match checks between decimal vaues may unexpectedly fail.

1.4.2. Bool

The sort Bool denotes logical values. Values are either true or false.

Premises on booleans
a == b
Equality check. Fails if the two booleans are not equal. a and b may be bound variables or boolean literals.
a != b
Inequality check. Fails if the two boolean are equal. a and b may be bound variables or boolean literals.
a => b
Equivalent to == if b is a boolean literal. Binds new variable b to the value of a if b is an unbound variable. Invalid if b is a bound variable.
a =!=> b
Equivalent to != if b is a boolean literal. Invalid if b is a variable (bound or unbound).
case a of { b => ... }
Switch-like premise for multiple cases. a must either be a boolean literal or a bound variable. b must either be a boolean literal or an unbound variable.

There are no built-in logical operations on the sort Bool. One can define meta-functions for these operations, for example:

module booleans

signature
  arrows
    not(Bool) --> Bool

rules
  not(true) --> false
  not(false) --> true

One can write reduction rules directly on boolean literals, for example:

module booleans

signature
  arrows
    Bool -not-> Bool

rules
  true -not-> false

  false -not-> true

1.4.3. String

The String sort denotes ASCII strings. The maximum length of a string is the maximum size of an Int.

string operations
building: “hello”, “hello world”
Builds a string from a literal
matching: a => “hello”, a =!=> “hello”
see == and != below
s1 == s2
Compare strings s1 and s2 for equality. Fail if the strings are not identical.
s1 != s2
Compare strings s1 and s2 for equality. Fail if the strings are identical.

1.4.4. List

The List terms denote list terms of homogenously typed terms. Use of a list sort must specify the sort of the contained elements. For example, the following declares a constructor foo having a list of integers as child:

module lists

signature
  sorts
    F
  constructors
    foo: List(Int) -> F
list operations
building: [], [a, b], [a, b | xs]

Build an empty list, a list of two elements and a list of two or more elements, respectively. If a, b and/or xs are variables they must be bound variables. If a is of sort S then b has to be of sort S and xs must be of sort List(S) or an empty list literal. Empty list literals - [] - are coercible to any list sort.

Examples of list build premises:

[] => x
[1, 2, 3] => x
[1, 2 | []] => x
[1, 2 | [3, 4]] => x
[a, b | [a, b]] => x
matching: [], [a, b], [a, b, c | xs], [_, _ | xs]

Matches an empty list, a list of two elements, a list of three or more elements and a list of two or more elements, respectively. All variables in a list match must be unbound variables. Variables occuring in the pattern will be bound if the entire pattern match succeeds. If any of a, b, c, xs is a term pattern (i.e. not a variable) then a pattern match will be attempted for that pattern.

Examples of list pattern matching premises:

t => []
t => [_, _]
t => [_, _ | _]
t => [1, 2]
t => [a, b | [c, d | xs]]
l1 == l2
Check lists l1 and l2 for equality. Two lists are equal if they are of the same type, they have the same length and being element-wise equal. Premise fails if the two lists are not equal.
l1 != l2
Check lists l1 and l2 for inequality. See above for a definition of list equality. Premise fails if the two lists are equal.
indexed access: l1[idx]
Retrieves the element at index idx in the list l1. Fails if the index is out of bounds.
concat: l1 ++ l2
Concatenates two lists of the same type: if the type of l1 is List(S), then the type of l2 has to be List(S), unless l2 is an empty list literal. The elements in the l2 list will be appended, in order, to the elements of l1.
reverse: `l1

Reverses the list l1. Example:

`[1, 2, 3] // => [3, 2, 1]
`[] // => []
`[1, 2, 3 | `[4, 5]] // => [4, 5, 3, 2, 1]

One may write reduction rules directly on list literals, but the type of the list has to be explicitly specified:

module lists

signature
  arrows
    List(Int) -empty-> Bool

rules
  [] : List(Int) -empty-> true

  [_|_] : List(Int) -empty-> false

1.4.5. Map

The sort Map denotes associative arrays, or dictionaries. A use of the map sort must declare the types of keys and the type of values. The following declares the sort Env as an alias to the sort mapping strings to integers:

signature
  sort aliases
    Env = Map(String, Int)

Note

Maps are immutable. Adding or removing entries from a map does not modify the existent map, instead it creates a new map.

map operations
building: {}, {k1 |–> v1}, {k1 |–> v1, k2 |–> v2, ...}
Build an empty map, a map with one entry and a map with multiple entries, respectively. All appearing variables must be bound. All keys must be of the same type, and all values must be of the same type. Results in a new map, the old map is unmodified.
extending: {k1 |–> v1, map}, {map, k1 |–> v1}
Extend the map represented by variable map with a new binding from key k1 to value v1. Entries on the left map replace entries with the same key on the right. Multiple additions can be performed at once: {k1 |--> v1, map, k2 |--> v2}. This is equivalent to writing: {k1 |--> v1, {map, k2 |--> v2}}. Multiple maps can be merged into one: {map1, map2, map3}. Again, the left entries replace the right entries. It is equivalent to writing: {map1, {map2, map3}}. The result is always a new map, the old map(s) remain(s) unmodified.
removing: map1 k1
Return a new map containing all entries in map map1 except for the entry with key k1. Fails if map1 has no entry for key k1. Map map1 remains unmodified.
access: map1[k1]
Return the value associated with key k1 in map map1. Fails if map1 does not have an entry for key k1.
contains: map1[k1?]
Check whether map map1 has an entry for key k1. Return true if an entry exists, false otherwise.
matching
Pattern matching is not possible on maps

Defining rules directly on maps is possible, but the type of the map has to be explicitly specified in the rule:

signature
  arrows
    Map(String, Int) -global-> Int

rules
  m : Map(String, Int) -global-> m["global"]

1.4.6. Tuple

The Tuple sort denotes pairs of terms of arbitrary (higher than 0) arity. Tuple sort usages must be accompanied by declarations of the types of their elements. For example:

signature
  sort aliases
    T = (S1 * S2 * S3)

declares sort T to be an alias of the 3-tuple of terms of type S1, S2 and S3, respectively.

tuple operations
building: (t1, t2, ...)
Build a tuple literal. All variables appearing in the construction must be bound. If the types of children t1, t2, ... are S1, S2, ..., respectively, then the type of the resulting tuple is (S1 * S2 * ...).
matching: (p1, p2, p3)
Match a term against a 3-tuple pattern. The patterns p1, p2, p3 are matched against the respective child of the incoming tuple. A tuple pattern match succeeds if the term matched is a tuple of equal arity and if the sub-pattern matches succeed. Variables appearing in the pattern must be unbound. Variables appearing in the pattern will be bound if the pattern match succeeds.

It is possible to define rules directly on tuple literals, but the type of the tuple has to be explicitly specified in the rule:

signature
  arrows
    (Bool * Bool) -or-> Bool

rules

  (true, _) : (Bool * Bool) -or-> true
  (_, true) : (Bool * Bool) -or-> true
  (false, false) : (Bool * Bool) -or-> false