LogStack

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.
== Instructions ==
Instruction	Effect
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.
== Computational Class ==
LogStack is Turing Complete, as proven by the following translation to 3-cell brainfuck, prefixed with ABC:
Brainfuck	LogStack
+ 	%
- 	%/(ab)(%A(%B(C/ab)(Bab)$/ab)(Aab)$ab)$
> 	(%@)%A(%B(C/ab)(Bab)$/ab)(Aab)$@
< 	(%@)%A(%B(C/ab)(Bab)$/ab)(Aab)$@(%@)%A(%B(C/ab)(Bab)$/ab)(Aab)$@
[ 	%(%/(
] 	%%ab)(%A(%B(C/ab)(Bab)$/ab)(Aab)$abc)$)
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.
== Use ==
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 p outputs 'no'.
* 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
== Examples ==
=== Truth Machine ===
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)
== External Resources ==
* Implementation
Category:Languages
Category:2020
Category:Stack-based
Category:Turing complete
Category:Output only
Category:Implemented