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").

Date: 2010-10-18 05:05 am (UTC)From: [identity profile] jokeserver.livejournal.com
But what about functions that operate on higher-order functions? Are they higherer-order functions?

Date: 2010-10-18 05:56 am (UTC)From: [identity profile] 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.

Date: 2010-10-18 01:51 pm (UTC)From: [personal profile] lindseykuper
lindseykuper: A figure, wearing a pink shirt decorated with a heart, looks upward from between dark shapes that suggest buildings. (Default)
Oh, "meta" gets used for this too. "It's taken for other purposes" never stopped anyone!

Date: 2010-10-18 03:54 pm (UTC)From: [identity profile] 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.

Date: 2010-10-18 04:16 pm (UTC)From: [identity profile] dachte.livejournal.com
It's very human for us to have invented all new ways to be frustrated!

Date: 2010-10-18 07:16 pm (UTC)From: [personal profile] lindseykuper
lindseykuper: A figure, wearing a pink shirt decorated with a heart, looks upward from between dark shapes that suggest buildings. (Default)
How about 'flavor'?

Date: 2010-10-18 06:44 am (UTC)From: [identity profile] redglasses.livejournal.com
HARMANZ

Date: 2010-10-18 08:15 am (UTC)From: [identity profile] 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!

Date: 2010-10-18 08:59 am (UTC)From: [identity profile] 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.

Date: 2010-10-18 05:51 pm (UTC)From: [identity profile] 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?

Date: 2010-10-18 07:29 pm (UTC)From: [identity profile] simrob.livejournal.com
Right - either functional abstract syntax or abstract functional syntax being "right" makes me reasonably convinced that I understand your point.

Date: 2010-10-19 04:54 pm (UTC)From: [identity profile] 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

Date: 2016-12-22 04:32 am (UTC)From: (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

Profile

chrisamaphone

August 2014

S M T W T F S
     12
3456789
10111213141516
17181920 21 2223
24252627282930
31      

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Oct. 21st, 2017 05:49 pm
Powered by Dreamwidth Studios