Logstack

From Esolang
Jump to navigation Jump to search

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:

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