-  [WT]  [PS]  [Home] [Manage]

[Return] [Entire Thread] [Last 50 posts] [First 100 posts]
>>
Predicate Logic as a programming language Lee 12/11/26(Mon)06:05 No. 3196

This publication has gone through many revisions, with the more recent ones using slightly less insightful notation. I found this early copy over at REMath

http://65.99.230.10:81/collect/computer/index/assoc/HASH0183.dir/doc.pdf

In short, we model problems as a system of "reverse" implication constraints inductively defined on the base order logic; to model computation, we attempt to disprove assertions that are known satisfiable in order to construct a counterexample.

For example, we can encode numerals as n \triangleq s^n(0) (here, 0 is some symbol and not the concrete number itself, this is very reminiscent of church encodings) so in order to calculate fib(n), we define a 2-ary predicate

fib(n,m)

to mean that m is the n-th fibonacci number. I.e, the following are true:
fib(0,0) <- fib(0) = 0
fib(1,1) <- fib(1) = 1
fib(1,2)
fib(2,3)
fib(3,4)
fib(5,5)

We can define the constraints that the fib predicate must follow as an inductive set

fib(0,0) <=
fib(1,1) <=

where P(x,...) <= means that P(x,...) holds vacuously, so here, we assert that there exists a symbol 0 such that 0 = fib(0); furthermore, 1 = s(0) = fib(1) as well.

Next, we have

fib(s(s(n)),u) <= fib(n,v), fib(s(n),w), add(v, w, u)

this says that if there exists some symbol v = fib(n) and some other symbol w = fib(n+1) (remember, n+1 is shorthand for s(n)) and if add(v,w,u) also holds, then there must exist some symbol u = fib(s(s(n))) (this just asserts that fib(s(s(n))) exists). Now, add(v,w,u) is a 3-ary rule stating that there exists some u such that u = v+w.

Now, to calculate fib(10), we would assert that

<= fib(10, u)

which says that if there exists u = fib(10), then nothing can be true, meaning that we're asserting that there does not exist u such that u = fib(10). We then work through our base order logic system either applying our rules or strengthening/weakening the system with "guesses" until we come across a counter-example


>>
Neckbearded Basement Dweller 12/11/28(Wed)15:55 No. 3216

Anyone have anything on Interprocess Communication in C.
More of a guide when and how to use what.
I've already read the Manuals(unistd.h, shm.h, mman.h, pthread.h) and resolved how to use shared memory with global memory and vfork(), but there doesn't seem to be much more than the manuals or guides how to use them.





Delete post []
Password  
Report post
Reason