Define meaning for symbol such as ⇓ despite 'Incomplete expression; more input is needed'

Question

Example

The notation $a\Downarrow_bc$ can mean something like "the program $a$ results in $c$ when executed according to the semantics of $b$".

In Mathematica, I input this as \[DoubleDownArrow] and use CTRL-- to write the underscript b. It can also be produced by DisplayForm@RowBox@{"a",SubscriptBox["\[DoubleDownArrow]","b"],"c"}.

a down b c

As 'boxes', this works (in strings, for instance). But since DoubleDownArrow is an infix operator, it fails to evaluate with the error "Incomplete expression; more input is needed". The $_b$ prevents the c from being interpreted as the right operand.

Question

What are flexible ways to

1. Remove errors which would otherwise occur for certain symbols/box expressions
2. Define meanings for certain symbols/box expressions
3. Create ways of outputting/inputting them

I'm interested in a variety of examples involving a variety of symbols. Ideally, every symbols with existing arities/interpretations could be tweaked: I'm thinking of creative uses of ∫, ⊢ and every other symbol you can think of.

In the case of $\Downarrow$, it would be nice to have $a\Downarrow_b c$ evaluate to a proposition, and it would be cool to have $a\Downarrow_b$ partially evaluate a as well.

An ambitious use case would be parsing python or other imperative code as symbols by overloading Dot and : and (/) etc; I think this is a gargantuan but possible task. The SymbolicC package already has the symbols to express an AST...

---

Editing of system files like in Edit UnicodeCharacters.tr-File is fine, but methods involving documented functions like Equivalent for \hookrightarrow, ↪ are preferred.

Answer 1

The basic form of the Wolfram Language is functional notation F[x,y,z], and the method of entering code is optimized for this. If you are fine with keeping the input as a function and only changing the output format (which is what I would do), I recommend preparing a three-variable function F[a,b,c] representing $a\Downarrow_b c$, and defining its output format as follows.

ClearAll[F]
Format[F[a_, b_, c_]] := 
 DisplayForm@RowBox@{a, SubscriptBox["\[DoubleDownArrow]", b], c}
F[a, b, c]

0

F[a, b, F[c, d, e]]

1

If what you want to do is something like automated theorem proving, I recommend using a program specialized for that purpose, such as Lean, rather than Mathematica.

Answer 2

Input alias for $a\Downarrow_b c$

We'll add an input alias so that escevalesc will produce an expression which looks like $a\Downarrow_b c$ but evaluate to ResultOfEvaluationIs:

CurrentValue[EvaluationNotebook[], {InputAliases, "eval"}] = 
 TemplateBox[{"\[SelectionPlaceholder]", "\[Placeholder]", "\[Placeholder]"}, 
 "", DisplayFunction :> (RowBox@{#, 
 SubscriptBox["\[DoubleDownArrow]", #2], #3} &), 
 InterpretationFunction :> (RowBox@{"ResultOfEvaluationIs",
 "[", RowBox@{"{", #, ",", #3, "}"}, ",", 
 RowBox@{"\"Semantics\"", "\[Rule]", #2}, "]"} &)]

partially typed input alias

Finishing with tab results in the visual notation. Its full form is

full form is ResultOfEvaluationIs

I can select the placeholders and populate them with contents.

populating placeholders of ResultOfEvaluationIs

Then the function can be defined, like ResultOfEvaluationIs[{a_,c_},"Semantics"->b_]:="Is it true that running "<>ToString@a<>" as "<>ToString@b<>" results in "<>ToString@b<>"?" .

---

I'm not sure how to make the \[SelectionPlaceholder] auto-selected -- my cursor is placed just after it rather than highlighting it, as happens with ctrl-- and other inputs.

Pretty printing to $a\Downarrow_b c$

Instead of evaluating, an "output form" can be added so that the expressions resulting from this input alias also appear with fancy boxes.

ResultOfEvaluationIs/:
MakeBoxes[ResultOfEvaluationIs[{a_,c_},"Semantics"->b_],f_]:=
TemplateBox[{MakeBoxes[a,f],MakeBoxes[b,f],MakeBoxes[c,f]},"",
DisplayFunction:>(RowBox@{#,
SubscriptBox["\[DoubleDownArrow]",#2],#3}&),
InterpretationFunction:>(RowBox@{"ResultOfEvaluationIs","[",
RowBox@{"{",#,",",#3,"}"},",",
RowBox@{"\"Semantics\"","\[Rule]",#2},"]"}&)]

My first attempt simply output the boxes directly; the resulting expression had the original problem. Every time one of these internal ResultOfEvaluationIs expressions is displayed, it 'wraps itself' in a TemplateBox so that it can be evaluated again to its internal ResultOfEvaluationIs form.

Cleaning up

I believe

CurrentValue[EvaluationNotebook[],InputAliases]= DeleteCases[CurrentValue[EvaluationNotebook[],InputAliases],"eval"->_]
FormatValues@ResultOfEvaluationIs=.
Remove@ResultOfEvaluationIs

Will make it like nothing ever happened in the kernel.