3
$\begingroup$

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.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
3
$\begingroup$

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.

Improve this answer
$\endgroup$

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.