higher-order snowclones

[chrisamaphone]

occasionally you'll hear someone ask, "are higher-order functions 'higher-order' in the same sense as higher-order logic?" here is a possible answer.

from my understanding of current logical diction, something like the following story is true:

once upon a time, humans invented lambda calculus. they said, "a function that takes a functional argument (or returns a functional value) is a higher-order function." they wrote that definition down, and then two different humans read it.

the first said, "ah! a 'higher-order' function is one that operates on a function. so, in general, for something to be 'higher-order' means it operates over functions."

the second said, "ah! a higher-order function is a function over functions. to generalize, a higher-order X is an X that operates over other Xes."

error! and from their teachings sprang many logician progeny of both lineages, and the confusion remains.

some examples:
- higher-order abstract syntax. "lam : (tm -> tm) -> tm" is higher order in that "oh look there's a left nested arrow", i.e. we're describing syntax in terms of function types (and for that reason may be better deserving of the abstract higher-order syntax coin).
- higher-order judgment. in twelf lingo we use this to mean, again, a judgment over open terms (like (tm -> tm) -> type) rather than what you might think following generalization (2), a judgment about judgments (i.e. a metatheorem).
- higher-order logic. if we squint for the sake of uniformity and pretend that by "logic" we mean "predicates", then i think it's accurate to interpret this as an instance of generalization (2), predicates over predicates. it certainly doesn't mean "logic about functional data", which is just propositional logic.

despite my NPOV efforts, it might be coming through that i'm a little annoyed with generalization 1. it just seems a little bit provincial or narrow-sighted, like the only thing that we could possibly want to get fancy with is the types of the things we describe, rather than the (quite literally) more judgmental-methodology-motivated notions of our system. of course, in practice, i use the jargon that will get me understood, but if i got to prescriptively reinvent it i'd change the word for generalization 1 to something like "functional" (where of course in this perfect universe, "functional programming" would be renamed to "value programming").

Comments

[jokeserver.livejournal.com]

But what about functions that operate on higher-order functions? Are they higherer-order functions?

[chrisamaphone]

nah -- "higher" is a fixed point.

[dachte.livejournal.com]

In some parts of philosophy we tend to use the word "meta" for these (second-meaning) purposes. Pity that's already taken for other purposes in programing.

[lindseykuper]

Oh, "meta" gets used for this too. "It's taken for other purposes" never stopped anyone!

[simrob.livejournal.com]

You should have witnessed my rage when I learned that category theorists (or somebody that talks to category theorists) had ascribed a specific meaning to variety, meaning there is literally non non-laden word that allows you to describe a class type kind sort set universe of stuff.

[dachte.livejournal.com]

It's very human for us to have invented all new ways to be frustrated!

[lindseykuper]

How about 'flavor'?

[simrob.livejournal.com]

I like it.

[wjl.livejournal.com]

nope, guess again

[lindseykuper]

Goddamn particle physicists.

[oniugnip.livejournal.com]

http://en.wikipedia.org/wiki/Kernel

[redglasses.livejournal.com]

HARMANZ

[roseandsigil.livejournal.com]

AARGH. Now I understand why it is called "higher order abstract syntax".

Definition 2 is the only correct definition! Down with definition 1!

[chrisamaphone]

rise up the polynomial hierarchy! all turing machines must be DESTROYED!

[rjmccall.livejournal.com]

Personally, I would generalize like so: an (n+1)th-order term contains abstraction over an nth order term (but no higher), and an nth-order language allows nth-order terms. In logic, terms are predicates, and abstraction over terms is quantification; in a λ-calculus, terms are expressions, and abstraction over terms is variable-binding.

This is perfectly reasonable except for the problem for academics that abstracting over functions doesn't add any theoretical complexity to a λ-calculus, whereas abstracting over predicates breaks completeness in a logic.

Anyway, I'm curious what the actual history of the term is, but I don't have JSTOR access anymore and can't read a lot of the relevant papers. Gödel proved the completeness of the first-order predicate calculus, but I'm pretty sure nobody called it that back then; that might date to Per Lindström's hierarchy of logics, but I can't see those papers. I don't think Church talks about the order of functions in his foundational papers at all.

[simrob.livejournal.com]

To be sure I've got you right (my own preconceptions clumsily wander in front of me, causing me to stumble), you would prefer for HOAS to be "Abstract Functional Syntax," yes?

[chrisamaphone]

either that or "functional abstract syntax"; i'm not quite sure. it's hard for even me to take these substitutions seriously in the midst of preconceptions. language, man, how does it work.

[simrob.livejournal.com]

Right - either functional abstract syntax or abstract functional syntax being "right" makes me reasonably convinced that I understand your point.

[wjl.livejournal.com]

We talked about this last night, but for the record/benefit of the audience:

Interestingly, higher-order judgment already has another meaning used by Twelf'ers, namely the judgment-level analogue of higher-order syntax:

  lam : (exp -> exp) -> exp.                    % higher-order syntax

  =>I : (true A -> true B) -> true (A => B).    % higher-order judgment/syntax?

  of/lam : ({x} of x A -> of (M x) B)
            -> of (lam [x] M x) (A => B).       % higher-order judgment

You said you'd just call this a "hypothetical judgment", which also makes sense (and is a kind of higher-order judgment itself!). Maybe we should call HOAS "hypothetical syntax"? :)

I think Frank uses "higher-level judgment" to describe your notion of "higher-order judgment": syntax is level 0, judgments about it are level 1, metatheorems are judgments at level 2, etc. A skew representation is one that mixes levels in the types of arguments, e.g. when your syntax requires proofs about syntax, or when your judgments themselves appeal to metatheorems.

Acquisition bargain penny-pinching tabs no medicament

[(Anonymous)]

overcoming ed
[url=http://pharmshop-online.com]generic cialis[/url] generic cialis online
generic cialis (http://pharmshop-online.com) - ed remedies
cialis 20 mg cost our newest member