On 19 Aug 2011, at 23:32, meekerdb wrote:

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?

Predicate are more syntactical object. They can be interpreted as function or relation, but in logic we distinguish explicitly the syntax and the semantics. So an arithmetical predicate is just a formula written with the usual symbols. Its intended meaning will be true or false, relatively to some model. For example, the predicate "x is greater than y" is "Ez(y+z = x)".

The semantics of combinators is rather hard, and it took time before mathematicians find one. D^D needs to be isomorphic to D, because there is only one domain (the collection of all combinators). But Dana Scott has solved the problem, and found a notion of continuous function making D^D isomorphic with D. Recursion theory provides also an intuitive model, where a number can be seen both as a function and a number: just define a new operation on the natural numbers: "@" by i @ j = phi_i(j). It is a bit nasty, given that such an operation will be partial (in case phi_i(j) does not stop).

Bruno





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 .


http://iridia.ulb.ac.be/~marchal/



--
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.

Reply via email to