hi friends,
I would like to ask for this question question,
What this mean ?
1) CAR(CONS(x,y)) = x
2) CDR(CONS(x,y)) = y
3) -| ATOM(x) ) CONS(CAR(x), CDR(x)) = x
4) -| ATOM(CONS(x,y))
thanks..
Edwin
The four formulas you posted formalize the relationship
between four functions named CONS, CAR, CDR, and ATOM,
and the equality symbol =. You should read them as
formulas of first order logic, with implicit universal
quantification of the variables x and y. The first two
formulas say that the arguments passed to CONS can be
recovered using CAR and CDR:
1) CAR(CONS(x,y)) = x
2) CDR(CONS(x,y)) = y
I suspect that your symbol "-|" is Heyting's symbol for
negation, which looks like a reverse "L" lying on its
side, and that the extra right parenthesis is material
conditional (only-if). Using the English words "not"
and "if ... then ..." instead, the third formula becomes
3) if not ATOM(x), then CONS(CAR(x), CDR(x)) = x
This says that if x is not an atom, then you can recover
the value of x by applying CONS to CAR(x) and CDR(x).
The fourth formula states that CONS(x,y) is not an atom:
4) not ATOM(CONS(x,y))
These four formulas, taken together, imply that CONS is
a pairing function with projections CAR and CDR.
The first three equations are not true of most real dialects
of Lisp, because most real dialects of Lisp have side effects
that allow the result of one call to CONS to be distinguished
from the result of a different call to CONS. Most real
dialects of Lisp also use Cambridge Polish syntax instead
of the prefix notation used in these equations.
Will
In article <·············@ccs.neu.edu> William D Clinger <····@ccs.neu.edu> writes:
> 1) CAR(CONS(x,y)) = x
> 2) CDR(CONS(x,y)) = y
> 3) if not ATOM(x), then CONS(CAR(x), CDR(x)) = x
> 4) not ATOM(CONS(x,y))
>
> These four formulas, taken together, imply that CONS is
> a pairing function with projections CAR and CDR.
>
> The first three equations are not true of most real dialects
> of Lisp, because most real dialects of Lisp have side effects
> that allow the result of one call to CONS to be distinguished
> from the result of a different call to CONS.
Actually, I think it is only #3 that isn't true of real dialects of
Lisp. Equations 1 and 2 hold as long as x and y have the same binding.
#3 is definitely not true for EQ, but is for EQUAL.
--
Thomas A. Russ, USC/Information Sciences Institute ···@isi.edu
In article <···············@hobbes.isi.edu>, ···@ISI.EDU (Thomas A. Russ) writes:
|> In article <·············@ccs.neu.edu> William D Clinger <····@ccs.neu.edu> writes:
|> > 1) CAR(CONS(x,y)) = x
|> > 2) CDR(CONS(x,y)) = y
|> > 3) if not ATOM(x), then CONS(CAR(x), CDR(x)) = x
|> > 4) not ATOM(CONS(x,y))
|> >
|> > These four formulas, taken together, imply that CONS is
|> > a pairing function with projections CAR and CDR.
If you add the induction axiom
5) if (P(a) for all a in A) and
(P(x) and P(y) imply P(CONS(x,y)))
then P(z) for all z in A union N
where A is the set of atoms, N is the non atoms in your model, and
P is a predicate. Now this set of axioms defines Peano integers
of the second kind. Here, CONS is the succesor function, and CAR
and CDR are both predecessor functions. (Forget for a moment that
most Lisps make CAR(nil) = CDR(nil) = nil and take a different view
on whether nil is in A or N.) With this system, we have the same
proof mechanisms for our programs that the logicans have for number
theory given the normal Peano axioms:
1+2) pred(suc(x)) = x
3) if x not 0, then suc(pred(x)) = x
4) not suc(x) = 0
5 if P(0) and P(x) implies P(suc(x))
then for all x, P(x)
BTW, I think this set of axioms was taught at MIT, in the early
1960s, to all Lisp hackers who wandered into a model theory
class.
Jeff Barnett
PS For those who want a challenge: What are all the finite models
of the above axioms? (Up to isomorphism, naturally.) Finite
means that both A and N are finite sets. In order to make this
meaningful, assume that axioms 1-4 are cast in a first order
language and that axiom 5 quantifies P in an extended logic that
allows such things. BTW, could you do this homework without axiom
5? Why or why not?
Edwin Chung wrote:
> I would like to ask for this question question,
> What this mean ?
>
> 1) CAR(CONS(x,y)) = x
> 2) CDR(CONS(x,y)) = y
> 3) -| ATOM(x) ) CONS(CAR(x), CDR(x)) = x
> 4) -| ATOM(CONS(x,y))
They're axioms for Lisp primitives CONS, CAR, CDR, and ATOM. Roughly,
speaking, they mean that the pair of functions CAR and CDR and the
function CONS are inverses. What you're typing as "-|" means "not", and
what you're typing as ")" means "if ... then ...". You can read the
axioms as follows:
1) the CAR of CONS(x, y) is x,
2) the CDR of CONS(x, y) is y,
3) if x is not an ATOM, then CONSing the CAR of x and the CDR of x
yields x, and
4) a CONS is not an ATOM.
-- rar
Edwin Chung <········@uwaterloo.ca> writes:
> What this mean ?
> 1) CAR(CONS(x,y)) = x
"For all terms x and y, CAR(CONS(x,y)) = x."
{CONS is a pairing function and CAR is the first projection.}
> 2) CDR(CONS(x,y)) = y
For all terms x and y, CDR(CONS(x,y)) = y.
{CONS is a pairing function and CDR is the second projection.}
> 3) -| ATOM(x) ) CONS(CAR(x), CDR(x)) = x
The "-|" is a "turnstile" meaning "it is provable that".
The " ) " should be a "horseshoe" with the open end facing left
(it is not a right parenthesis)
and means "implies".
This means
"It is provable that
for all terms x
if x is an ATOM then
CONS(CAR(x), CDR(x)) = x"
and I am sure you have this wrong, because CAR and CDR are defined
on pairs, not atoms. It should be
3) NOT ATOM(x) => CONS(CAR(x),CDR(x)) = x
which means
"CONS is a pure function; if you take a pair (NOT ATOM) apart
using CAR and CDR and build a new pair using CONS, you get the
same pair you started with."
This is not true in Lisp. (EQUAL (CONS (CAR X) (CDR X)) X) is true,
but they are not the same shape.
> 4) -| ATOM(CONS(x,y))
"It is provable that
for all terms x, y
CONS(x, y) is an atom."
Again, I think you have omitted a negation sign here, because an atom is
that which has no parts (is "a-tomos" (not cuttable)). No pair is an
atom and no atom is a pair. It should probably read
NOT ATOM(CONS(x,y))
which says "a pair is not an atom".
Basically, what you have here, somewhat mangled, are the conventional
axioms for pairs, simultaneously defining four functions:
CONS(x,y) make a pair with first component x
and second component y
CAR(pair) return the first component of a pair
(not defined on non-pairs)
CDR(pair) return the second component of a pair
(not defined on non-pairs)
ATOM(x) true if and only if x is NOT a pair.
--
Australian citizen since 14 August 1996. *Now* I can vote the xxxs out!
Richard A. O'Keefe; http://www.cs.rmit.edu.au/%7Eok; RMIT Comp.Sci.