User:Hppavilion1/Combinatory temporal logic
It is part of User:Hppavilion1's series of variants on things like combinatory logic to make them more interesting.
Combinatory temporal logic is based off of linear (single-path) temporal logic and combinatory logic. It borrows the syntax from combinatory logic and the timey wiminess from temporal logic. As such, it is really just SK with some new combinators for temporal manipulation, as well as a slight adjustment to the way assignment works (builtin (not just convention for ease of reading), anonymous).
Roughly, the grammar is:
combinator ::= Combinator_Symbol ; # NOT a parenthesis app ::= exp exp ; parenexp ::= "(" exp ")" ; assignment ::= Combinator_Symbol "=" expression ; expression ::= assignment | parenexp | app | combinator ;
A combinator is a combinator symbol, which means a symbol that is NOT a parenthesis (well, this isn't defined in the above grammar, but it's implied). An application is the concatenation of two expressions. A parenthetical expression is an expression padded in parentheses. An assignment is a single combinator symbol, followed by an "equals" sign, followed by an expression. Finally, an expression is either an assignment, a parenthetical expression, an application, or a lone combinator. This definition is, obviously, recursive.
In normal combinatory logic, the grammar is as such:
combinator ::= Combinator_Symbol ; app ::= exp exp ; parenexp ::= "(" exp ")" ; expression ::= app | parenexp | combinator ;
Notice that assignment is not builtin to the grammar; it is a convention adopted to make reading easier. This is different in combinatory temporal logic, where assignment is an expression. Furthermore, assignment is part of the single universal expression type. This seems normal, until one realizes that this means that assignment can be used anywhere a normal combinator can be used. This means that, for example,
K(I=SKK) is a valid expression. This differs in semantics from normal combinatory logic, because now one can use assignments as combinators. Because of the semantics of combinatory temporal logic,
I=SKK (for example) literally means the assignment of
SKK, as opposed to something like assignments returning the combinator they define.
Combinatory temporal logic has the traditional
SK(I) combinators. As a refresher:
S = λxyz.xz(yz) K = λxy.x I = SKK
In addition to these, there are some additional "temporal" combinators that allow the programmer to manipulate time state and such. These combinators are still being determined, but currently they are:
||Alpha Combinator||"αύριο" ("tomorrow")||Assert that x holds at the following state||
|| Make |
||Step-identity ("alpha") combinator||"βxήμα" ("step")|| Equivalent to
||Go to the next state|