The derivability of a given statement can be justified by exhibiting a derivation tree [...] For example, if

[ some definitions ]

then the derivability of the statement

if t then false else false --> if u then false else false

is witnessed by the following derivation tree:

(Types and Programming Languages by Benjamin C. Pierce)

Does witnessed here means the same as is justified from above?

More examples from the same book:

Indeed, the derivation trees witnessing evaluation statements will always have this slender form: since no evaluation rule has more than one premise, there is no way to construct a branching derivation tree.


In the simple type system we are dealing with in this chapter, every term has a single type (if it has any type at all), and there is always just one derivation tree witnessing this fact.

  • 2
    I really wish you had picked a different example, because I'm hung up on its redundancy. (There is no reason for a such a construction if the conclusion will always be false. Just state an axiom: false.) It's making it difficult for me to place the word contextually. Also, witnessed is not a word that would normally be used here. Things are witnessed by conscious beings—not by "derivation trees." – Jason Bassford Sep 3 '18 at 17:32
  • 1
    @JasonBassford I've added two more examples from the same book – DevNewb Sep 3 '18 at 17:54
  • @Jason Bassford You are wrong about this: Things are witnessed by conscious beings—not by "derivation trees." The Cambridge Guide to English Usage, for example, is full of sentences like these: Stopless acronyms/initialisms are normal in the world of computing, witness ASCII, CD-ROM etc. Imperial expressions of length, height and depth vary between singular and plural, witness six foot five versus six feet five inches as the height of the local giant. – Michael Login Sep 3 '18 at 18:10
  • 1
    @MvLog In your example, witness ASCII, CD-ROM etc. is a declaration for the unstated you (the reader) to witness something. It's no different than the sentence Stop!. I guarantee, it cannot be interpreted as having the ASCII, CD-ROM, or whatever do any witnessing. – Jason Bassford Sep 3 '18 at 23:09
  • 1
    @MvLog Idiomatic usage is quite different from syntactical composition that sticks things together that shouldn't be. – Jason Bassford Sep 4 '18 at 14:46

In this context, the tree can not justify the statement, because the tree is in fact derived from the statement (so the justification would involve cyclical logic). Instead, the tree seems to depict or visualize [the structure of the statement].

“Indeed, the derivation trees depicting evaluation statements...”

| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.