XPost: sci.math
From: janburse@fastmail.fm
Hi,
We can though prove in FOL:
∀y∃!x x = f(y)
Another example with existence,
that doesn't boil down to unique
existence, is this here:
∃x∃y(x = f(y))
One might find it in Prolog as
X = f(_) with an anonymous variable _.
Now its not possible to derive:
/* Not Generally Valid */
∃!x∃y(x = f(y))
Bye
Mild Shock schrieb:
> Hi,
>
> A Prolog logical variable is not immutable,
> it transitions all the time from uninstantiated
> to instantiated, during unification.
>
> Also the value the logical variable represents
> is not immutable, since it might point to a
> Prolog term which is non-ground, this
>
> Prolog term might have other Prolog logical variables,
> which do also such transitions, making the
> while Prolog term transitioniong from less ground
>
> to more ground, or even worse to a larger
> term with even more Prolog logical variables,
> and so on, leading to the phaenomenon of
>
> perpetual processes or concurrent logic programming.
> In particular the existence quantifier ∃ in logic
> programming is not unique existence ∃!. For
>
> example the following is true:
>
> ∃x x = f(y)
>
> But x has not a "single value", the existence
> is more witness to of a kind of skolem function
> dependency, namely that for each y, there
>
> is some f(y). What they write is only useful
> for a certained moded form of Prolog and unification,
> where the equations have unique existence of
>
> ground terms or some other value domain.
>
> Bye
>
> Mild Shock schrieb:
>> Hi,
>>
>> Its their take of Logical variable, which
>> might not be the same as a Prolog logical variable.
>>
>> ------------------ cut here ----------------
>>
>> 2.1 Logical variables and equations
>> A program executes by solving its equations, using
>> the process of unification. For example,
>>
>> ∃x y z. x = ; x= <2,z>; y
>>
>> is solved by unifying x with and with <2, z>;
>> that in turn unifies with <2, z>, which unifies
>> y with 2 and z with 3. Finally, 2 is returned as the
>> result. Note carefully that, as in any declarative
>> language, logical variables are not mutable; a logical
>> variable stands for a single, immutable value.
>>
>> We use "∃" to bring a fresh logical variable into
>> scope, because we really mean "there exists an x
>> such that .... "
>>
>> ------------------ cut here ----------------
>>
>> Of course the above is utter nonsense, written
>> from somebody who doesn't know what a Prolog logical
>> variable is, shifting in the same sentence from
>>
>> the attribution of "immutable" of a variable, to
>> the attribution of "immutable" of the value
>> of a variable. This is quite hillarious.
>>
>> Bye
>>
>> Mild Shock schrieb:
>>> Hi,
>>>
>>> Its from this paper:
>>>
>>> The Verse Calculus:a Core Calculus for Functional Logic Programming
>>> SIMON PEYTON JONES, Epic Games, United Kingdom
>>> GUY STEELE, Oracle Labs, USA
>>> https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf
>>>
>>> Don't blame me for what they write.
>>> But mostlikely your eruption is just from
>>> a clueless Nazi Retard, namely the paid
>>>
>>> troll you are, getting money from Putin.
>>>
>>> Bye
>>>
>>> Franz Sneijders schrieb:
>>>> Mild Shock wrote:
>>>>
>>>>> We use “∃” to bring a fresh logical variable into scope, because we
>>>>> really mean “there exists an x such that ···.”
>>>>
>>>> idiot, there is no any x over there. And it doesn't need to be a
>>>> variable,
>>>> a constant suffices.
>>>>
>>>
>>
>
--- SoupGate-Win32 v1.05
* Origin: you cannot sedate... all the things you hate (1:229/2)
|
