LogStack is a stack-based logic language created by User:Silver. Each item on the stack is a valid sentence of propositional logic, and all conditionals work by popping one and testing whether it can be proven using the rest of the stack as assumptions.
|a-zA-Z||push an atomic proposition corresponding to the letter|
|*||push a contradiction|
|%||push a tautology|
|&||pop two propositions p and q, and push a compound proposition 'p and q'|
||||pop two propositions p and q, and push a compound proposition 'p or q'|
|!||pop a proposition and push its negation|
|^||pop two propositions p and q and push 'p xor q'. This is syntactic sugar, under the hood all compound propositions are in terms of and, or and not|
|:||pop two propositions p and q and push 'q implies p' (in that order, so "ab:" pushes a=>b)|
|=||pop two propositions p and q and push 'p if and only if q' (biconditional)|
|/||swap the top two items on the stack|
|;||duplicate the top item on the stack|
|$||pop and discard|
|@||rotate the stack - pop an proposition and place it on the bottom of the stack|
|~||pop a proposition and try to prove it using the rest of the stack. If it is provable, swap the top two items (not replacing the proposition popped for testing)|
|?||pop a proposition and try to prove it. output the result ('yes' or 'no')|
|()||loop - before each iteration, pop a proposition and try to prove it. If it's not provable, end the loop immediately|
|.||halt the program|
|#||output the state of the stack, mostly for debugging purposes|
Any other character will be ignored.
LogStack is Turing Complete, as proven by the following translation to 3-cell brainfuck:
Which isn't as ugly as it looks (quite) once you realise that much of it is repeated
%A(%B(C/ab)(Bab)$/ab)(Aab)$, which figures out which of A,B or C have just been popped and pushes the right one back.
As it turns out, the logic part isn't that much use. A subset of the language consisting only of three atomic propositions, %, /, $, @ and () is Turing Complete, as shown above. However, there are a couple of useful things to remember:
- The difference between false and unprovable matters.
p?on a stack that makes no mention of
- The principle of explosion applies. If the stack implies a contradiction, all propositions are provable. This breaks the constructions below if it happens.
- the construction
%/( [if true] ab)( [if false] ab)$acts as an if-else statement
- the construction
*( [comment] )allows comments
Truthy input for this program consists of a starting stack containing a single 'p', falsy input is an empty starting stack.
p *(push (another?) 'p') ( *(pop something, initially the 'p' we just pushed, and try to prove it. If it's not provable, skip past the matching ')') pp?) *(push two 'p's, then pop one of them and output whether or not it's provable - always yes. Then go back to the '(') a? *(push 'a' and output whether it's provable - always no, since it's not mentioned anywhere in the stack)