[FOM] Question about "fresh" variables/objects in logics
A. Mani
a_mani_sc_gs at yahoo.co.in
Sat Nov 26 12:40:11 EST 2005
On Friday 25 November 2005 21:01, 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
This is a fresh composition.
All that means there are translations of partial interpretations (in the
algebraic sense).
Fresh(x, X) iff (\forall {y}\in X)(\forall{v}\inV)(v(y)=z --->y\neq x)
V is a set of partial monic functions defined by your context :X --> Z,
You can use the multisorted version.
On X you need a concept of notequality only.
v(y)=z means v(y) is defined.
Now unless you make a few relaxations, your 'fresh' will remain that way.
> The formal description of this concept would help me a lot. I am doing
> research in functional programming and I could use it there.
>
AFAIK if you change types of values and manipulate them...it is unique to
functional programming. It is "one-way" in formal logic...translations are
developed in that direction. But ...you can make the model differently.
A. Mani
Member, Cal. Math. Soc
More information about the FOM
mailing list