Parsing Polish notation

Richard Suchenwirth 2001-10-29 - Reading a book on logics this weekend, I felt challenged to implement a "translator" from Polish (prefix) notation to the conventional logic notation, which is easily done with Tcl and its Unicode support.

Both notations have their advantages. Polish notation as introduced by Jan Lukasiewicz, where operators (capital letters) precede their operands, is extremely compact, free of parentheses and yet unambiguous, and can easily be entered on a keyboard, but are hard to read, e.g.

 ECpqCNqNp "if and only if p implies q, then not-q implies not-p"

Conventional notation is more intuitive and closer to algebraic formulas, but uses special characters that you need a good Unicode font for. Here is a comparison:

 Name               Polish  Conventional symbol
 negation("not")        N   right-then-down stroke
 conjunction("and")     K   like A without horizontal
 alternation("or")      A   like V
 implication("then")    C   arrow pointing right(->)
 equivalence("iff")     E   left-right arrow(<->)

Polish notation is best parsed from right to left (that's why Reverse Polish Notation is more popular - see RPN in Tcl), so first I reverse the order of the PN symbols. Then it's very easy with a stack to process the symbols - note the custom ppop command that adds parentheses to its output if it needs them. This way I could keep the translator short ;-)

 proc polish2convent'l polish {
    foreach i [lrevert [split $polish ""]] {
            switch -- $i {
                A       {push s "[ppop s] \u2228 [ppop s]"}
                C       {push s "[ppop s] \u2192 [ppop s]"}
                E       {push s "[ppop s] \u2194 [ppop s]"}
                K       {push s "[ppop s] \u2227 [ppop s]"}
                N       {push s "\u2510[ppop s]"}
                default {push s $i}
            }
    }
    pop s
 }
 proc lrevert {list} {
    set res {}
    foreach i $list {set res [concat [list $i] $res]}
    set res
 }
 proc push {name what} {upvar 1 $name s; lappend s $what}
 proc pop {name {- ""}} {
    upvar 1 $name s
        set res [lindex $s end]
        set s [lrange $s 0 end-1]
        set res
 }
 proc ppop {name {- ""}} {
    upvar 1 $name s
        set res [uplevel pop $name]
        if {[string length $res]>4} {set res ($res)}
        set res
 }
 # -- self-test demo
 if {[file tail $argv0]==[file tail [info script]]} {
    pack [text .t]
    foreach i {
        NKpNp CNpCpq CCpqCNqNp CKpNpq ENNpp EApqNKNpNq
    } {.t insert end [format %-15s\t%s\n $i: [polish2convent'l $i]]}
 }

This story continues in A little proving engine