User:Hppavilion1/Combinatory temporal logic

Combinatory temporal logic is a variant of combinatory logic that is inspired by Temporal logic that someone might someday want to use for an esolang.

It is part of User:Hppavilion1's series of variants on things like combinatory logic to make them more interesting.

Design

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).

Grammar

Roughly, the grammar is:

combinator ::= Combinator_Symbol ;  # NOT a parenthesis
app        ::= exp exp ;
parenexp   ::= "(" exp ")" ;
assignment ::= Combinator_Symbol "=" expression ;
expression ::= assignment | parenexp | app | combinator ;

English

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.

The Difference

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 I to SKK, as opposed to something like assignments returning the combinator they define.

Combinators

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:

Information				Example
Combinator	Name	Name Origin	Meaning	Usage	Effect
αx	Alpha Combinator	"αύριο" ("tomorrow")	Assert that x holds at the following state	α(B = S(KS)K)	Make B equal to S(KS)K) (the standard B combinator) at the next state, and from then on until redefined
βx	Step-identity ("alpha") combinator	"βxήμα" ("step")	Equivalent to I, except it steps to the next state	βK	Go to the next state