On 8/19/2011 2:18 AM, Bruno Marchal wrote:
So do you have a LISP program that will make my computer Lobian?
It would be easier to do it by hands:
1) develop a first order logic specification for your computer (that
is a first order axiomatic for its data structures, including the
elementary manipulations that your computer can do on them)
2) add a scheme of induction axioms on those data structure. For
example, for the combinators, it would be like this
"if P(K) and P(S) and if for all X and Y P(X) & P(Y) implies P((X,Y))
then for all X and Y P((X,Y))". And this for all "P" describable in
your language.
Just to clarify P is some predicate, i.e. a function that returns #T or
#F and X and Y are some data stuctures (e.g. lists) and ( , ) is a
combinator, i.e. a function from DxD =>D for D the domain of X and Y.
Right?
Brent
It will be automatically Löbian. And, yes, it should not be to
difficult to write a program in LISP, doing that. That is, starting
from a first order logical specification of an interpreter, extending
it into a Löbian machine.
Bruno
--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To post to this group, send email to everything-list@googlegroups.com.
To unsubscribe from this group, send email to
everything-list+unsubscr...@googlegroups.com.
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en.
