[FOM] Question about "fresh" variables/objects in logics

[Bas Spitters]

On Friday 25 November 2005 16:31, Divianszky Peter wrote:
> Does anybody know of a formal description of the concept of "fresh"
> variable/object in logic?
>
> This concept is used in theoretical computer science quite often, but I
> have never seen a formal description of it.
> Informally it could be descibed as:
>
> Let X be an infinite set.
> The definition
>    x in X is fresh
> means that
>    x is an element of X
>   and
>    for all y in X defined elsewhere: x not equal y
>
> The formal description of this concept would help me a lot. I am doing
> research in functional programming and I could use it there.

There's much active work in this direction. Check the Merlin workshop's, for 
instance. There are implementions and libraries for both Haskell and OCaml.

Bas