I'm trying to understand John McCarthy's 1996
http://www-formal.stanford.edu/jmc/towards/node8.html
which refers to '60s publications, which I can't access:
John McCarthy. Checking mathematical proofs by computer. In
Proceedings Symposium on Recursive Function Theory (1961).
American Mathematical Society, 1962.
and
A basis for a mathematical theory of computation. In
P. Braffort and D. Hirschberg, editors, Computer Programming
and Formal Systems, pages 33-70. North-Holland, Amsterdam,
1963.
He writes:-
> 3. Conditional expressions satisfy a number of identities, and a
> complete theory of conditional expressions, very similar to
> propositional calculus, is thoroughly treated in [[9]McC63]. We shall
> list a few of the identities taken as axioms here.
>
> 1. (if true then a else b) = a
> 2. (if false then a else b) = b
which follows from the definition of
'if p then a else b'; where 'p' is a predicate/boolean and
'a' , 'b' are statements.
Importantly (IMO) 'b' can be substituted for
'(if false then a else b)'.
I'm hoping this all leads to substitutions transforming programs,
which will make proving correctness possible/easier ?
> 3. if p then (if q then a else b) else (if q then c else d)
> =if q then (if p then a else c) else (if p then b else d)
This can be confirmed by evaluating the results for each the 4 values of
p.q: 00,01,10,11 for which I get d, c, b, a respectively, for both
expresssions, so the 2nd expresssion can substitute for the 1st.
> 4. f(if p then a else b) = if p then f(a) else f(b)
Not only can I not prove this, I don't even know what it means.
Let's try:
f(x) means the image of x under the mapping/function 'f'.
The mapping/function 'f' is a set of ordered pairs: (domain,img).
So apparently 'if p then a else b' is an element of the domain ?
And 'if p then f(a) else f(b)' is the corresponding image ?
I guess McCarthy proved this one of his 60s papers ?
Let's see what *TYPE* of elements he is dealing with ?
In http://www-formal.stanford.edu/jmc/basis.html
[A Basis for a Mathematical Theory of Computation]
he writes:
...it includes a systematic theory of conditional expressions, a
treatment of their recursive use and the method of recursion
induction for proving properties of recursively defined functions.
So, I guess the domain of 'f' above is a "conditional expression" ?
As is the image: 'if p then f(a) else f(b)' ?
Conventionally I'd define a & b as statements, but looking at his
later material, it seems that they are expressions.
Is the missing background to these questions available online ?
Thanks for any feedback, [ "?" indicates a question ;-) ]
== Chris Glur.
On Feb 29, 5:37 pm, ········@gmail wrote:
> I'm trying to understand John McCarthy's 1996http://www-formal.stanford.edu/jmc/towards/node8.html
> which refers to '60s publications, which I can't access:
> John McCarthy. Checking mathematical proofs by computer. In
> Proceedings Symposium on Recursive Function Theory (1961).
> American Mathematical Society, 1962.
> and
> A basis for a mathematical theory of computation. In
> P. Braffort and D. Hirschberg, editors, Computer Programming
> and Formal Systems, pages 33-70. North-Holland, Amsterdam,
> 1963.
>
> He writes:-
> > 3. Conditional expressions satisfy a number of identities, and a
> > complete theory of conditional expressions, very similar to
> > propositional calculus, is thoroughly treated in [[9]McC63]. We shall
> > list a few of the identities taken as axioms here.
>
> > 1. (if true then a else b) = a
> > 2. (if false then a else b) = b
Too many arguments to special form IF.
Unbound variables, TRUE, THEN, A.
> > 4. f(if p then a else b) = if p then f(a) else f(b)
>
> Not only can I not prove this, I don't even know what it means.
It means that a function over if/then/else distributes into the
consequent and alternate. Just like multiplication distributes over
addition:
a*(b + c) = a*b + a*c
Suppose that f(x) is a function that multiplies by a, f(x) = a * x.
Then we can rewrite the distributive law as:
f(b + c) = f(b) + f(c)
Of course, we can't just write it like this without defining what f
is, because it does not hold for any f.
What McCarthy is asserting is that ANY function will distribute into
the if/then/else.
We intuitively know this from Lisp programming.
Given:
;; make a list containing the symbol ODD if X is odd,
;; otherwise a list containing EVEN:
(if (oddp x) (list 'odd) (list 'even)))
;; briefer code equivalent to above:
(list (if (oddp x) 'odd 'even)))
How can you prove this? Since it's so self evident, this should be
trivial. Firstly, let's use the Lisp synax, which doesn't have the
bullshit THEN and ELSE in it. And let's use T and NIL instead of true
and false, while we are at it, and the notation (f x) for f(x). We
have this:
Axioms:
(if t x y) = x (1)
(if nil x y) = y (2)
Transitive rule axiom:
a = b and b = c -> a = c (3)
Goal is to prove:
(f (if p a b)) = (if p (f a) (f b))
This calls for division into cases:
case 1: p is NIL, i.e. (null p)
;; substitute a for x in (2), and substitute b for y:
(if p a b) = b (4)
;; apply f to both sides of (4)
(f (if p a b)) = (f b) (5)
;; substitute (f a) for x in (2), and substitute (f b) for y:
(if p (f a) (f b)) = (f b) (6)
;; By transitive rule (3), since (5) and (6) each equate
;; a quantity to (f b) those two quantities are equal:
(f (if p a b)) = (if p (f a) (f b)) (7)
case 2: p is T
;; proved in similar way:
;; apply f to both sides of (4)
(f (if p a b)) = (f a) (8)
;; substitute (f a) for x in (2), and substitute (f b) for y:
(if p (f a) (f b)) = (f a) (9)
;; By transitive rule on (8) and (9):
(f (if p a b)) = (if p (f a) (f b)) (10)
But (10) from case 2 is the same equation as (7) from case 1, and is
identical to the the equation we are trying to prove. Thus the
equation is true: it holds in both cases, regardless of the value of
p.
["Followup-To:" header set to comp.lang.lisp.]
On 2008-03-01, Kaz Kylheku <········@gmail.com> wrote:
> Axioms:
>
> (if t x y) = x (1)
> (if nil x y) = y (2)
>
> Transitive rule axiom:
>
> a = b and b = c -> a = c (3)
>
> Goal is to prove:
>
> (f (if p a b)) = (if p (f a) (f b))
>
> This calls for division into cases:
>
> case 1: p is NIL, i.e. (null p)
>
> ;; substitute a for x in (2), and substitute b for y:
> (if p a b) = b (4)
>
> ;; apply f to both sides of (4)
> (f (if p a b)) = (f b) (5)
>
> ;; substitute (f a) for x in (2), and substitute (f b) for y:
> (if p (f a) (f b)) = (f b) (6)
Before you can perform Step 6, you have to assume that (f (if p a b)) =
(if p (f a) (f b)), or else you can't substitute one for the other.
Hi,
> > ;; substitute (f a) for x in (2), and substitute (f b) for y:
> > (if p (f a) (f b)) = (f b) (6)
>
> Before you can perform Step 6, you have to assume that (f (if p a b)) =
> (if p (f a) (f b)), or else you can't substitute one for the other.
Which is why that's not what step 6 does. :)
Note that (6) is not based on (5), but on axiom (2).
~ Matthias
On 1 Mar, 01:37, ········@gmail wrote:
> I'm trying to understand John McCarthy's 1996http://www-formal.stanford.edu/jmc/towards/node8.html
> which refers to '60s publications, which I can't access:
> John McCarthy. Checking mathematical proofs by computer. In
> Proceedings Symposium on Recursive Function Theory (1961).
> American Mathematical Society, 1962.
> and
> A basis for a mathematical theory of computation. In
> P. Braffort and D. Hirschberg, editors, Computer Programming
> and Formal Systems, pages 33-70. North-Holland, Amsterdam,
> 1963.
>
> He writes:-
> > 3. Conditional expressions satisfy a number of identities, and a
> > complete theory of conditional expressions, very similar to
> > propositional calculus, is thoroughly treated in [[9]McC63]. We shall
> > list a few of the identities taken as axioms here.
>
> > 1. (if true then a else b) = a
> > 2. (if false then a else b) = b
>
> which follows from the definition of
> 'if p then a else b'; where 'p' is a predicate/boolean and
> 'a' , 'b' are statements.
> Importantly (IMO) 'b' can be substituted for
> '(if false then a else b)'.
>
> I'm hoping this all leads to substitutions transforming programs,
> which will make proving correctness possible/easier ?
>
> > 3. if p then (if q then a else b) else (if q then c else d)
> > =if q then (if p then a else c) else (if p then b else d)
>
> This can be confirmed by evaluating the results for each the 4 values of
> p.q: 00,01,10,11 for which I get d, c, b, a respectively, for both
> expresssions, so the 2nd expresssion can substitute for the 1st.
>
> > 4. f(if p then a else b) = if p then f(a) else f(b)
>
> Not only can I not prove this, I don't even know what it means.
> Let's try:
> f(x) means the image of x under the mapping/function 'f'.
> The mapping/function 'f' is a set of ordered pairs: (domain,img).
> So apparently 'if p then a else b' is an element of the domain ?
> And 'if p then f(a) else f(b)' is the corresponding image ?
> I guess McCarthy proved this one of his 60s papers ?
>
> Let's see what *TYPE* of elements he is dealing with ?
> In http://www-formal.stanford.edu/jmc/basis.html
> [A Basis for a Mathematical Theory of Computation]he writes:
>
> ...it includes a systematic theory of conditional expressions, a
> treatment of their recursive use and the method of recursion
> induction for proving properties of recursively defined functions.
>
> So, I guess the domain of 'f' above is a "conditional expression" ?
> As is the image: 'if p then f(a) else f(b)' ?
>
> Conventionally I'd define a & b as statements, but looking at his
> later material, it seems that they are expressions.
>
> Is the missing background to these questions available online ?
>
> Thanks for any feedback, [ "?" indicates a question ;-) ]
>
> == Chris Glur.
The best people for this are Boyer & Moore in 'A Computational Logic'
and their successor publications who really went into this in depth.
Its a tough but rewarding read.
Mark
On 2008-03-01, in sci.logic, ········@gmail wrote:
>> 4. f(if p then a else b) = if p then f(a) else f(b)
>
> Not only can I not prove this, I don't even know what it means.
The expression "if p then a else b" evaluates to a if p evaluates to
true and to b otherwise, so the above just says that f(k), where k is
the value of "if p then a else b", is f(a) if p evaluates to true and
f(b) otherwise.
--
Aatu Koskensilta (················@xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
On Feb 29, 7:37 pm, ········@gmail wrote:
> > 4. f(if p then a else b) = if p then f(a) else f(b)
> Not only can I not prove this, I don't even know what it means.
Just wait 'til you see stuff like
(if p then f else g)(x)
:)
> So, I guess the domain of 'f' above is a "conditional expression" ?
No, not any more than the domain of printf contains an
arithmetic expression in
printf("%d", a + b);
-------------------------------
Dan Bensen
http://www.prairienet.org/~dsb/
From: Chris Barts
Subject: Re: McCarthy's Proving Statements About Recursive Functions
Date:
Message-ID: <87prueinv5.fsf@chbarts.home>
········@gmail writes:
> Let's see what *TYPE* of elements he is dealing with ?
> In http://www-formal.stanford.edu/jmc/basis.html
> [A Basis for a Mathematical Theory of Computation]
> he writes:
> ...it includes a systematic theory of conditional expressions, a
> treatment of their recursive use and the method of recursion
> induction for proving properties of recursively defined functions.
>
> So, I guess the domain of 'f' above is a "conditional expression" ?
> As is the image: 'if p then f(a) else f(b)' ?
No, it means that the conditional gets evaluated first because arguments
are always evaluated before they get passed to functions. You really need
to understand that (if x then a else b) is an *expression* with a *value*,
just like (+ 5 6) and (sum (list 1 2 3 4 5)). Lisp doesn't have statements
like Fortran and Algol do.
>
> Conventionally I'd define a & b as statements, but looking at his
> later material, it seems that they are expressions.
*Everything* is an expression. Lisp isn't line-oriented, it's sexp-oriented,
and a sexp always notates an expression.
Maybe this isn't the theoretical explanation you're looking for. It is,
however, the one likely to help you understand Lisp and how Lisp is
fundamentally different from most other languages.