Lambda the Ultimate

This page is a wonderful collection of deeply nested kennings, Nordic circumlocations. They were actually used! And people were supposed to understand them, real time, in oral recitation.

Example:
Sóknrýrir vann sextán herðimeiða hríðar mána viðar hauðrmens sára.
The destroyer of attackers wounded sixteen increasers of storm of moon of tree of land-necklace.

land-necklace = ocean
tree of ocean = ship
moon of ship = shield
storm of shield = battle
increaser of battle = warrior

The destroyer of attackers wounded sixteen increasers of storm of moon of tree of land-necklace

There are still only a small number of recursions there, and I believe the slight stretching of comprehensibilty both recursively and through the transitive generation of poetic tropes is an intentional part of the poetic device, meant to display eloquence.

The extra opacity we perceive is because we are unfamiliar with the poetic tradition: the constituent images would have been as familiar to their intended audience as scene cuts in film and TV are to us.

An interesting example nonetheless. I notice that as Lauri predicted, these deeper recursions are tail recursions.

This one demonstrates a kind of mutual recursion between "sword" and "shield", where shield is expressed in terms of sword in terms of shield in terms of sword. It's a sort of multi-level eta expansion (not quite the right term but I can't think of a better one). In OCaml:

type shield = Shield
type sword = Sword

let ness (x:sword) = Shield;;
let harmer (x:shield) = Sword;;
let path (x:sword) = Shield;;

let f x = path (harmer (ness x));;

Type inference tells us that f is a function from sword to shield:

val f : sword -> shield = <fun>

So assuming that all phrases which denote 'shield' are equivalent, we can just insert the shortest one, replacing "læbraut eiðs lögðis" with, perhaps, "hlífar", if we're willing to risk the wrath of a group of people who spend an inordinate amount of time inventing complex recursive synonyms intended to glorify words like "warrior"...

Type inference tells us that f is a function from sword to shield:

I think you just set a new record for PLT nerdiness with that one, Anton.
;-)

Quite!

The idea of using type systems for analysing natural language is not actually very exotic. Look up e.g. Montague grammars for a concrete example.

And everyone knows computational linguists aren't nerdy at all...

Marc's just nervous because he realizes I might finally be onto a mathematical proof of Sapir-Whorf!

And everyone knows computational linguists aren't nerdy at all...

Hey... I resemble that remark!

Marc's just nervous because he realizes I might finally be onto a mathematical proof of Sapir-Whorf!

If anyone needs me I'll be cowering under my desk...

(See what happens when we start discussing linguistics on LtU...)

Not to be outdone on the nerdiness scale, it just struck me that what we have going on here is actually unification:

A = B of C
C = D of E
E = F of G

therefore B of D of F of G = A

So I guess we actually need to write an Oz or Prolog program to handle this more naturally...

"This statement is false." Depending on evaluation strategy, isn't that an infinite recursion?

Since I assume you must currently be in an infinitely loop thinking about this sentence, I won't interrupt you by responding. ;-)

No problemo! There are benefits to being of above-Turing intelligence. Or maybe that's being presumptuous... :-)

I find it much simpler just to not bother with consistency... or soundness for that matter.

"This statement is false." Depending on evaluation strategy, isn't that an infinite recursion?

There is no syntactic recursion in that sentence. The issue at hand is whether all languages have syntactic recursion.