# IDP4 playground

IngmarDasseville
2,434 views

## (Anonymous) functions

While writing down theories, it is very common that multiple expressions take on the same form. Luckily it is possible to abstract these away using functions.

Note that function application is done by just writing a space between the function and the argument.

Functions
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
//Functions with one argument
f x := 3*x + 4.
a := f 5 - f 6.
b := (3*5+4) - (3*6+4).
a = b.
//Functions with multiple argument
g x y := x * y + 2.
c := g 7 8.
d := 7*8 + 2.
c = d.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Warning: Equality and comparisons between functions is not guaranteed to give any useful result.

It is also possible to use infix notation for binary function application. In this case you need to write your function name between backticks a plus b

Infix Functions
1
2
3
4
5
plus a b := a + b.
c := 3 plus 4.
relevant c.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

### Anonymous Functions

It is also possible to define a function and not give it a name, this is done with a backslash. Note that just like let-constructs, functions also introduce a local scope so the x within the function definition is not the same as the x we are defining.

Anonymous Functions
1
2
3
x := (\x -> x + 1) 3.
x = 4.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

A function declaration: f a b := g a b is actually syntactical sugar for f := (\a -> (\b -> g a b)).

### Currying

If a function takes two arguments, it is not necesary to apply them to both at once. You can reuse a partially applied function multiple times like this:

Currying
1
2
3
4
5
6
7
g x y := 3*x*y - 2*y.
f := g 5.
x := f 6 + f 7.
x = g 5 6 + g 5 7.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

### The other way around

#### Functions

Similarly to constraints with variables, IDP4 allows the introduction of unknown functions that take a value satisfying the given constraints. You can declare a function with the statement: name/arity :: function to setExpression.

Uninterpreted Functions
1
2
3
4
5
f/1 :: function to {1..10}.
f 3 > 3.
f 5 < 5.
f 3 + f 5 = 3 + 5.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

#### Predicates

A special case are Boolean functions, also known as predicates. Again, as with propositions, IDP4 has efficient support predicates through the declaration name/arity :: predicate.

Predicates
1
2
3
4
5
f/1 :: predicate.
f 4 | f 5.
~(f 6 & f 5).
f 4 => f 6.
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
Open Source Your Knowledge: become a Contributor and help others learn.